 \documentclass[preprint,11pt]{elsarticle}
 
\usepackage{intestazione2}
\usepackage{macron}
%\usepackage{geometry}
\usepackage{times}
\usepackage{mathpartir}


\begin{document}
 
\begin{frontmatter}
\title{Disciplined Structured Communications with \\ 
%Consistent
Disciplined Runtime Adaptation}
%\title{Disciplined Adaptation for Structured Communications}
\author[evry]{Cinzia Di Giusto} 
\author[unl]{Jorge A. P\'{e}rez}

%\cortext[cor1]{Corresponding author}  
\address[evry]{Universit\'e d'Evry - Val d'Essonne, Laboratoire IBISC}
\address[unl]{CITI and Departamento de Inform\'atica, FCT Universidade Nova de Lisboa}


     
\begin{abstract}
\emph{Session types} offer a powerful type-the\-o\-ret\-ic foundation for the analysis of 
structured communications, as commonly found in serv\-ice-oriented systems.
They are defined upon core programming calculi which offer only limited support 
for expressing adaptation and evolvability requirements.
This is unfortunate, as serv\-ice\--ori\-ented systems are increasingly being deployed upon 
highly dynamic infrastructures in which such requirements are 
central concerns.
In previous work, we developed a process calculi framework of \emph{adaptable processes},
in which concurrent processes can be replaced,  suspended, or discarded at runtime.
In this paper, we 
propose a session types discipline for a calculus with adaptable processes. 
Our typed framework offers an alternative for integrating runtime adaptation mechanisms in 
the modeling and analysis of structured communications.
We show that 
well-typed processes enjoy \emph{safety} and \emph{consistency} properties:
while the former ensures the absence of communication errors at runtime, the latter
guarantees that active session behavior is never disrupted by adaptation actions.
\end{abstract}

\end{frontmatter}

\section{Introduction}

\emph{Session types} 
offer a powerful type-theoretic foundation  
for the analysis of 
complex scenarios of structured communications, as frequently found in service-oriented systems.  
They abstract communication protocols as basic interaction patterns, which 
are then statically checked against specifications
in some core programming calculus---typ\-i\-cal\-ly, a variant of the $\pi$-calculus~\cite{DBLP:journals/iandc/MilnerPW92a}. 
Introduced in~\cite{DBLP:conf/concur/Honda93,DBLP:conf/esop/HondaVK98}, 
session type theories 
%have received much attention and 
have been extended in many directions---see~\cite{DBLP:conf/wsfm/Dezani-Ciancaglinid09} for a survey. 
Their practical relevance %of session types 
is witnessed by, e.g., 
 their recent application in the verification of parallel systems~\cite{DBLP:conf/tools/NgYH12}.

In spite of these developments, 
we find that existing ses\-sion-typed
calculi do not explicitly support 
%for reasoning about 
mechanisms for 
\emph{runtime adaptation}. 
While channel mobility (also known as \emph{delegation}~\cite{DBLP:journals/entcs/YoshidaV07}) 
as supported by such calculi
is often useful to model forms of
dynamic reconfiguration, more general forms of adaptation/evolvability 
are not expressible or are hard to reason about.
%Adaptation and evolvability are increasingly relevant issues nowadays, 
Runtime adaptation is an increasingly relevant issue nowadays, 
as distributed systems and applications are  being deployed in
open, highly dynamic infrastructures, such as cloud computing platforms.
In such settings,  
runtime adaptation %and dynamic reconfiguration  
appears as a key feature to
ensure continued system operation,
reduce costs, and achieve
business agility. 

We thus observe a rather unfortunate discrepancy between 
(i)~the evolvability capabilities of modern communicating systems in practice, and 
(ii)~the forms of interaction available in 
%the calculi upon which session types disciplines are defined.
(typed) process frameworks developed to reason about the correctness of such systems.


In this paper, we propose a simple approach towards overcoming this discrepancy.
We %extend an existing 
introduce a
session types discipline 
for a language
equipped
with 
mechanisms for runtime adaptation.
Rather than developing yet another session types discipline \emph{from scratch}, we have deliberately 
preferred to build upon existing lines of work. 
Our proposal 
builds upon
%results from combining 
the framework of 
\emph{adaptable processes}, 
an attempt for enhancing process calculi specifications with evolvability mechanisms
which we have developed together with Bravetti and Zavattaro in~\cite{BGPZFMOODS}.
We combine the constructs for adaptable processes with
the main insights %principles %underlying the discipline 
of the session type system
put forward by Garralda et al.~\cite{DBLP:conf/ppdp/GarraldaCD06} for the Boxed Ambient calculus~\cite{DBLP:journals/toplas/BugliesiCC04}.
Since the type system in~\cite{DBLP:conf/ppdp/GarraldaCD06} does not handle delegation, 
we  support this important mechanism by relying on the ``liberal'' typing system described in~\cite{DBLP:journals/entcs/YoshidaV07}.
As a result of this integration of concepts, 
we obtain a simple yet expressive model 
of structured communications with explicit mechanisms for runtime adaptation.


We briefly describe our approach and results. 
Our process language includes
the usual $\pi$-calculus constructs for session communication, but extended 
with the \emph{located processes} and the \emph{update processes} introduced in~\cite{BGPZFMOODS}.
Given a location $l$, a process $P$, and a context $Q(\mathsf{X})$ 
(i.e. a process $Q$ with free occurrences of variable $\mathsf{X}$), these processes are noted $l[P]$ and 
$\adapt{l}{Q}{X}$, respectively. 
%$l\{Q(\mathsf{X})\}$, resp. 
They may synchronize on $l$ so as to evolve into process 
$Q\subst{P}{\mathsf{X}}$ ---the process $Q$ in which all free occurrences of $X$ are replaced with $P$.
This interaction represents the \emph{update} of  process $P$ at $l$ with an \emph{adaptation routine}
(or built-in adaptation mechanism)
embodied by $Q(\mathsf{X})$. Locations can be nested and are transparent:
within $l[P]$, process $P$ may evolve autonomously, with the potential of interacting with some neighboring 
update process for $l$. 
%$l\{Q(\mathsf{X})\}$, 
%$\adapt{l}{Q}{X}$,
%as just described, 
Hence, 
in our language communicating behavior coexists with update actions. 
This raises the need for disciplining both forms of interaction, in such a way that 
 session types descriptions are respected and  evolvability requirements are enforced. 
To this end, by observing that %exploiting the fact that 
our update actions are a simple form of (higher-order) process mobility, 
we draw inspiration from the session types 
in~\cite{DBLP:conf/ppdp/GarraldaCD06}, 
which ensure that
sessions within Ambient hierarchies %are \emph{safe}, i.e., they 
are never disrupted by Ambient mobility steps.
By generalizing this insight to the context of (session) processes which execute
in arbitrary, possibly nested locations, we obtain a property which we call \emph{consistency}:
update actions over located processes which are engaged in active session behavior cannot be enabled.

%While both Ambients and adaptable processes rely on nested located processes,
%Ambient mobility and evolvability steps are conceptually very different.
%In fact, %is a major difference:
%Ambient mobility is only defined in a parent-child style, whereas
%located processes and update actions 
% may interact independently of their relative position in the hierarchy induced by location nesting.
%This way, integrating our calculus for adaptable processes %of~\cite{BGPZFMOODS} 
%with the session types discipline in~\cite{DBLP:conf/ppdp/GarraldaCD06}
%roughly amounts to: 

To show how
located and update processes fit in a session-typed process language, 
and to illustrate our  notion of consistency, 
we  consider a simple distributed client/server scenario,
% of distributed, interacting services (a client $C_1$ and a replicated service $S$), 
conveniently represented as located processes:
\begin{eqnarray*}
\mathsf{Sys} & \triangleq &  %\scomponent{l_{0}}{C_1} \para 
\scomponent{l_{1}}{C_1} \para\bigscomponent{l_2}{\scomponent{r}{S} \para R \, } \quad\text{where:} \vspace{3mm} \\ 
C_1  &  \triangleq  & \nopenr{a}{x}.\outC{x}{u_1,p_1}.\select{x}{n_1.P_1}.\close{x} \\
S  &  \triangleq  & \repopen{a}{y}.\inC{y}{u,p}.\branch{y}{n_1{:}Q_1 \parallel n_2{:}Q_2}.\close{y} 
\end{eqnarray*}
Intuitively, 
$\mathsf{Sys}$ 
consists of a replicated server $S$ and a client $C_1$, hosted in different locations $l_1$ and $r$.
They 
may  establish a session %of type $\sigma$ 
%between $S$ and $C_1$ %($i \in \{0, 1\}$) 
using name $a$:
first, the client sends its credentials to the server; then, the client chooses one of the 
services offered by the server. 
Above, the actual client and server behaviors are  abstracted by processes $P_1$ and $Q_1$, respectively.
%(resp. $P_1$ and $Q_1$), 
%which are left unspecified.
Finally, server and client synchronize to close the session.
Process  $R$, in location $l_2$, represents the platform in which  $S$ is deployed.

Starting from $\mathsf{Sys}$, let us suppose that a new session is indeed established by synchronization on $a$. 
Our semantics decrees the following reduction step:  %We then have
\begin{eqnarray*}
\mathsf{Sys} \!\!\!& \pired & \!\!\!\! (\nu \kappa)\big(\scomponent{l_{1}}{\outC{\kappa^{+}}{u_1,p_1}.\select{\kappa^{+}}{n_1.P_1}.\close{\kappa^{+}}} \para \\ 
& & \quad \bigscomponent{l_2}{\scomponent{r}{\inC{\kappa^{-}}{u,p}.\branch{\kappa^{-}}{n_1{:}Q_1 \parallel n_2{:}Q_2}.\close{\kappa^{-}} \para S\,} \para R \, }\big) = \mathsf{Sys}'
\end{eqnarray*} 
where 
$\kappa^+$ and $\kappa^-$ denote the two \emph{end-points} of channel $\kappa$~\cite{DBLP:journals/acta/GayH05}.
Suppose now that $R$ simply represents an upgrade process, which is ready to synchronize with $r$, the location in which $S$ resides: 
$$R = \adaptn{r}{NewS(\mathsf{X})}$$
From $\mathsf{Sys}'$, an update on $r$ would be  inconvenient for at least two reasons:
\begin{enumerate}[(a)]
\item First, since $r$ contains the local server behavior for an already established session, 
a careless update action on $r$ could potentially discard such behavior. This would leave the client in $l_1$ without a partner---the  protocol agreed upon session establishment would not be respected. 
\item Second, since $r$ contains also the actual service definition $S$, an undisciplined 
update action on $r$ could 
affect the service on $a$ in a variety of ways---for instance, it could destroy it. 
This clearly goes against the expected nature of services, which should be always available. 
\end{enumerate}

Above, item (a) concerns our intended notion of consistency, which ensures that any update actions on $r$
(such as those involving $R$ above) are only enabled  when $r$ contains no active sessions. 
Closely related, item (b) concerns a most desirable principle for services, namely that ``services should always be available in multiple copies''---this is the Service Channel Principle (SCP) identified in~\cite{DBLP:conf/esop/CarboneHY07}.


\paragraph{Contributions} In this context, our typed framework lies upon two main technical contributions:
\begin{enumerate}[(1)]
%\item generalizing the operational semantics of~\cite{DBLP:conf/ppdp/GarraldaCD06}
%so as to account for adaptation in \emph{arbitrary process hierarchies}; 
\item An \emph{operational semantics} for  our session language with located and update processes~\cite{BGPZFMOODS}.
The semantics enables adaptation actions within  \emph{arbitrary process hierarchies} and, following~\cite{DBLP:conf/ppdp/GarraldaCD06}, 
endows each located process with a suitable \emph{runtime annotation}, which describes its active session behavior.
Runtime annotations for locations are key in avoiding undesirable update actions such as the described in~(a) above.

%conservatively extending the typing system in~\cite{DBLP:conf/ppdp/GarraldaCD06}, so as to be able to reason about \emph{process interfaces}.
\item A \emph{typing system} which extends existing session types systems~\cite{DBLP:journals/entcs/YoshidaV07,DBLP:conf/ppdp/GarraldaCD06}
with the notion of \emph{interfaces}, which allow for simple and intuitive static checking rules for evolvability constructs. 
In particular, interfaces are of the essence in avoiding careless updates such as the described in (b) above.
This typing system provides a static analysis technique for ensuring 
\emph{safety}, i.e., absence of communication errors at runtime, but also 
consistency, as described above.
\end{enumerate}

%Ultimately, this last step is what realizes a form of \emph{typeful adaptation}, which contrasts with the untyped adaptation in~\cite{BGPZFMOODS}.  Well-typed processes 
%in our framework
%satisfy basic correctness guarantees (formalized as a Subject Reduction result), 
%which entails consistency for session-typed processes %that
%with runtime adaptation mechanisms.
%
%\jp{Perhaps adding an example of 'wrong' updates/consistency, to be addressed via static analysis?}


%\jp{This paragraph fits better at the end...}



\paragraph{Organization}
%The paper is structured as follows.
Next, in Sect.~\ref{sec:syn}, we present our process language, 
a session calculus with adaptable processes.
In Sect.~\ref{s:types} we present our session type system, and 
in Sect.~\ref{sec:res} we define and investigate its main properties, namely  safety and consistency. 
We illustrate our typed approach via examples in Sect.~\ref{sec:exam}, where we revisit the client/server scenario discussed above.
In Sect.~\ref{sec:int} we discuss extensions and enhancements for typing, in particular refinements for our notion of  interfaces.
Finally, Sect.~\ref{sec:rw} discusses related work and Sect.~\ref{sec:conc} collects some concluding remarks.

This paper is a revised version of the conference paper~\cite{DBLP:conf/sac/GiustoP13}, extended 
with further examples, discussions, as well as with proofs of the main technical results. %\footnote{Process $\adapt{l}{Q}{X}$ was written $l\{Q(\mathsf{X})\}$ in \cite{DBLP:conf/sac/GiustoP13}.}
With respect to~\cite{DBLP:conf/sac/GiustoP13}, in this presentation the operational semantics and typing system
have been much simplified. For instance, while in~\cite{DBLP:conf/sac/GiustoP13} the operational semantics was
instrumented with several elements that supported the static analyses (following~\cite{DBLP:conf/ppdp/GarraldaCD06}), 
the semantics given here is much lighter and relies only on a simple runtime annotation for located processes---the other elements are now subsumed by the (revised) typing discipline. Moreover, Sect.~\ref{ss:examp}, which illustrates runtime adaptation patterns
in an untyped setting, is new to this presentation, whereas 
 Sects.~\ref{sec:exam},~\ref{sec:int}, and~\ref{sec:rw} have been expanded significantly.



% 
 \section{A Process Language with Runtime Adaptation}\label{sec:syn}
We extend standard session-typed languages (see, e.g.,~\cite{DBLP:conf/esop/HondaVK98,DBLP:journals/entcs/YoshidaV07})
with \emph{located processes} and \emph{update actions}~\cite{BGPZFMOODS}.
These constructs allow us to explicitly represent adaptation mechanisms 
as part of models of structured communications.
In this section, we introduce the syntax and semantics of our process model, 
and illustrate some of the adaptation patterns expressible in it.
%\jp{As I explain below, we could (and probably should) avoid saying the following sentence.}
%As in~\cite{DBLP:conf/ppdp/GarraldaCD06}, 
%our process language 
%is instrumented with some elements which support the static analysis.
%In particular, we  
%annotate 
%located processes with an integer (representing established sessions).

\subsection{Syntax}
Our syntax builds upon the following  (disjoint)
base sets: 
\emph{names}, ranged over $a, b, x, y, \ldots$;
\emph{locations}, ranged over $l, l', \ldots$;
\emph{labels}, ranged over $n, n', \ldots$;
\emph{process variables}, ranged over $\mathsf{X}, \mathsf{X}', \ldots$;
\emph{constants} (integers, booleans, names), ranged over $c, c', \ldots$.
%The sets of names and locations are assumed disjoint.
Then, \emph{processes}, ranged over $P, Q, R, \ldots$
and \emph{expressions}, ranged over $e, e', \ldots$
are given by the grammar in Table \ref{tab:syntax}.
Our semantics uses 
\emph{(polarized) channels}, ranged over $\cha^{p}, \cha_1^{p}, \ldots$ (with $p \in \{+,-\}$)
and \emph{integers}, ranged over $j,h,m,\ldots$.
We use identifier $k$ to denote  channels $\cha^{p}$ and names $x$.

%\emph{recursion variables}, ranged over $Y, Y', \ldots$;



\begin{table}[t]
$$
\begin{array}{lrlr}
P & ::=  &   \nopenr{a}{x}.P  & \text{session request}	\\
	& \sepr &   \nopena{a}{x}.P  & \text{session acceptance: linear}	\\
	       & \sepr & \repopen{a}{x}.P  & \text{session acceptance: persistent}	\\
	& \sepr &  \outC{k}{\tilde{e}}.P & \text{data output}\\
  	&\sepr &    \inC{k}{\tilde{x}}.P  & \text{data input}\\
	& \sepr &  \throw{k}{k'}.P & \text{channel output}\\
    &\sepr &   \catch{k}{x}.P  & \text{channel input}\\
	&\sepr&   \select{k}{n};P & \text{selection}\\
    	&\sepr&   \branch{k}{n_1{:}P_1 \parallel \cdots \parallel n_m{:}P_m} & \text{branching}\\
%	&\sepr&  \component{l}{h}{\Delta}{P} ~~(h \geq 0)  & \text{adaptable process}\\
	&\sepr&  \scomponent{l}{P}   & \text{adaptable process}\\
	&\sepr&  \adapt{l}{P}{X}  %\sepr \migrate{l}{m}  \sepr  \destroy{l} 
	& \text{update process}\\
	    & \sepr &   \mathsf{X}& \text{process variable} \\
  	& \sepr &  \ifte{e}{P}{Q} & \text{conditional}\\
  	& \sepr &   P \para  P & \text{parallel composition}\\	 
		&\sepr&   \close{k}.P & \text{close session}	\\
			&\sepr&   \restr{k}{P}  & \text{channel hiding}	\\
			&\sepr&   \mathbf{0}  & \text{inaction} \\
%p	&::= &  + \sepr - &\text{channel polarities} \\
e	&::= &  c &\text{constants} \\
    & \sepr &   e_1 + e_2 \sepr e_1 - e_2  \sepr \ldots & \text{arithmetic expressions}
\end{array} 
$$
\caption{Process syntax.} \label{tab:syntax}
\end{table}


We comment on constructs in Table~\ref{tab:syntax}; 
intuitions and conventions for most constructs are as expected~\cite{DBLP:conf/esop/HondaVK98}.
Prefixes $\nopena{a}{x}$  and $\nopenr{a}{y}$ use name $a$ to establish a new session;
prefix $\close{k}$ is used to explicitly terminate session $k$. 
Having this prefix is crucial to our approach, for it allows us to keep track of the open sessions at any given time.
%\jp{We should hint why this is crucial to our approach.}
Once established, structured behavior on channels is possible.
 The exchange of expressions is as usual; channel passing  
(delegation) is also supported.
Thus, our language includes the usual dynamic reconfiguration via channel passing
as well as the more expressive runtime adaptation via \emph{located} and \emph{update processes}, as we discuss below.
For the sake of simplicity,
we consider infinite behavior in the form of replicated services, rather than as recursive definitions;
we do not foresee difficulties in extending our static analyses to a language with recursion.
Also for simplicity, we consider a restriction operator over channels only---restriction over names is not 
supported.
%included because we want full transparency.}
%\todo{dire anche qualcosa sul fatto che non c'e' restriction per i session name o per i locality name}


%\newpage
%\todo{nel type system abbiamo associato ad ogni locality l un interfaccia (un tipo) preciso, forse si puo' gia' dire qualcosa qui}

As hinted at in the Introduction, a \emph{located process} $\scomponent{l}{Q}$ denotes a
process $Q$  deployed at location $l$.
Inside $l$, process $Q$ can evolve on its own and interact with external processes.
In $\scomponent{l}{Q}$, we use $l$ as a reference for a potential update action, which 
occurs by interaction with an \emph{update process} $\adapt{l}{P}{X}$---a built-in adaptation mechanism.
In $\adapt{l}{P}{X}$, 
we use $P(\mathsf{X})$ to denote a process $P$ with zero or more occurrences of process variable $\mathsf{X}$.
%Intuitively,
As formalized by the operational semantics in Sect.~\ref{ss:opsem},
an \emph{update action} at $l$ corresponds to 
 the interaction of $\scomponent{l}{Q}$ and $\adapt{l}{P}{X}$ which leads to process 
$P\subst{Q}{\mathsf{X}}$---the process $P$ in which free occurrences of $\mathsf{X}$ are substituted with $Q$.  
In the semantics, we shall consider \emph{annotated} located processes 
$\component{l}{h}{\Delta}{Q}$, where $h$ stands for the number of active sessions in $Q$.
This runtime annotation is used by the type discipline in Sect.~\ref{s:types} to ensure that 
update actions do not disrupt the active session behavior deployed at a given location---this is the \emph{consistency} guarantee, formally addressed in Sect.~\ref{ss:consist}. %, we shall refer to this guarantee as \emph{consistency}.
%Furthermore, for each location $l$, the typing discipline assigns and maintains 
%a \emph{(service) interface} which succinctly describes the  services deployed at $l$.
%The intention is that any update actions on $l$ should at least maintain the service offer as described by its interface.

%$\component{l}{h}{\Delta}{Q}$. 
%$h$ stands for the number of active sessions in $Q$: 
%our operational semantics uses this information to ensure that locations enclosing active 
%sessions are not interrupted by update actions (consistency). 
%\jp{A better approach is to introduce syntax of located processes \emph{without} annotations, saying that $h$ is generated at runtime,
%and that our semantics is instrumented to use $h$.}


%\jp{The following is a bit different now:} In fact, as explained  below, 
%if the \emph{interfaces} of $Q$ and $P$ are 
%\emph{compatible} then 
%processes $\component{l}{h}{\INT_1}{Q}$ and $\adapt{l}{P}{X}$
%may interact so as to \emph{evolve} into $Q\subst{P}{\mathsf{X}}$.  
% Thus, 
% intuitively,
% process $\updated{l}{X}{\INT_1}{\INT_2}{Q}$ 
% behaves as a function which 
% expects a process with interface compatible with $\INT_1$ and 
% returns an adapted process with interface $\INT_2$.

Notions of binders  are as follows: 
the channel variable $x$ is bound in processes 
$\nopenr{a}{x}.P$, ~$\repopen{a}{x}.P$, and $\nopena{a}{x}.P$; similarly, 
$\tilde{x}$ is bound in $\inC{k}{\tilde{x}}.P$ (variables $x_1, \ldots, x_n$ are all distinct). 
Also, process variable $\mathsf{X}$ is bound in the update process $\adapt{l}{P}{X}$.
This way, sets of free and bound channels and process variables of a process $P$---noted $\mathsf{fc}(P)$, $\mathsf{fv}(P)$, $\mathsf{bc}(P)$, and $\mathsf{bv}(P)$, respectively---are defined as expected. 
%We define  $\mathsf{fu}(P) \triangleq \mathsf{fn}(P) \cup \mathsf{fc}(P)$.
%The treatment of recursion variables is also as customary. 
%As for process variables, we assume update processes bind process variables in it. 
%\jp{Free process variables??}
In all cases, we rely on usual notions of $\alpha$-conversion (noted $\equiv_\alpha$) and (capture-avoiding, simultaneous) substitution, noted
$\sub{\tilde{c}}{\tilde{x}}$ (for data), $\sub{\kappa^p}{\tilde{x}}$ (for channels), and $\sub{P}{\mathsf{X}}$ (for processes).
We work only with closed processes, and often omit the trailing $\nil$.

\subsection{Semantics}\label{ss:opsem}
%\todo{Spiegare bene quando compaiono i Kappa, i kappa compaiono a runtime}

The semantics of our process language is given by 
a \emph{reduction semantics},
denoted $P \pired P'$, the smallest relation on processes generated by the rules in Table~\ref{tab:semantics}.
As customary, it relies on  
an evaluation relation on expressions (noted $e \downarrow c$) and on
a structural congruence relation,  denoted $\equiv$, which we define next.

\begin{definition}[Structural Congruence]
Structural congruence is  
the smallest congruence relation on processes that is generated by the following laws:
$$
\begin{array}{cc}
P \!\para \! Q \!\equiv\! Q \!\para \! P  &
(P \!\para \! Q) \!\para \! R \!\equiv\! P \!\para \! (Q \!\para \! R) \\
P \!\para \! \nil \!\equiv\! P  & 
P \!\equiv\! Q \text{ if } P \!\equiv\!_\alpha Q \\
\restr{\cha}{\nil} \!\equiv\! \nil & \restr{\cha}{\restr{\kappa'}{P}} \!\equiv\! \restr{\cha'}{\restr{\cha}{P}} \\
\restr{\cha}{P} \!\para \! Q \!\equiv\! \restr{\cha}{(P \!\para \! Q)} ~~\text{(if $\cha \not\in \mathsf{fc}(Q)$)} &
\restr{\cha}{\component{l}{h}{\Delta}{P}} \!\equiv\! \component{l}{h}{\Delta}{\restr{\cha}{P}} 
\end{array}
$$
\end{definition}

\begin{table}[t]
{
$$
\begin{array}{ll}
 \rulename{r:Open} & 
E\big\{C\{\nopena{a}{x}.P\} \para  D\{\nopenr{a}{y}.Q\}\big\} \pired  \\
& 
\hfill E^{++}_{} \big\{\restr{\cha}{\big({C^{+}_{}\{P\sub{\cha^+}{x}\}  \para  D^{+}_{}\{Q\sub{\cha^-}{y}\} }\big)\big\} } \vspace{2.0mm} \\
\rulename{r:ROpen} & 
E\big\{C\{\repopen{a}{x}.P\}  \para  D\{\nopenr{a}{y}.Q\} \big\}  \pired  \\
& 
\hfill E^{++}_{}\big\{\restr{\cha}{\big({C^{+}_{}\{P\sub{\cha^+}{x}  \para \repopen{a}{x}.P \}  \para  D^{+}_{}\{Q\sub{\cha^-}{y}\} }\big)}\big\}  
 \vspace{2.0mm}\\
\rulename{r:Upd} & 
E\big\{C\{\component{l}{0}{}{Q}\} \para  D\{\adapt{l}{P}{X}\}\big\} 
\pired   \\
& \hfill 
E_{}\big\{C\{P\sub{Q}{\mathsf{X}}\}  \para  D\{\nil\}\big\} \vspace{ 1.5mm} \\
% \srulename{r:Move} & 
% E\big\{C\{\component{l}{h}{}{Q}\} \para  D\{\migrate{l}{m}\}\big\}~~ \pired   
% E_{}\big\{C\{\component{m}{h}{}{Q}\}  \para  D\{\nil\}\big\} \vspace{ 1.5mm} \\
% \srulename{r:Kill} & 
% E\big\{C\{\component{l}{0}{}{Q}\} \para  D\{\destroy{l}\}\big\}~~ 
% \pired   
% E_{}\big\{C\{\nil\}  \para  D\{\nil\}\big\} \vspace{ 1.5mm} \\
\rulename{r:I/O} &
E\big\{C\{\outC{\cha^{\,p}}{\tilde{e}}.P\} \para  D\{\inC{\cha^{\,\overline{p}}}{\tilde{x}}.Q\}\big\} 
\pired \\
& \hfill 
E\big\{C\{P\} \para  D\{Q\sub{\tilde{c}\,}{\tilde{x}}\}\big\} \quad (\tilde{e} \downarrow \tilde{c}) \vspace{ 1.5mm}
\\
\rulename{r:Pass} &
E\big\{C\{\throw{\cha^{\,p}}{\cha'^{\,q}}.P\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.Q\}\big\}\pired \\
& \hfill E\big\{C^{-}\{P\} \para  D^{+}\{Q\sub{\cha'^{\,q}}{x}\}\big\} \vspace{ 1.5mm}
\\
\rulename{r:Sel} &
E\big\{C\{\branch{\cha^{\,p}}{n_1{:}P_1 \parallel \cdots \parallel n_m{:}P_m}\} \para  D\{\select{\cha^{\,\overline{p}}}{n_j};Q\}\big\} 
\pired \\
& 
\hfill E\big\{C\{P_j\}\para  D\{Q\}\big\}  \quad (1 \leq j \leq m)  \vspace{ 1.5mm}
\\
\rulename{r:Close} &
E\big\{C\{\close{\cha^{\,p}}.P\} \para  D\{\close{\cha^{\,\overline{p}}}.Q\}\big\} \pired \\
& \hfill E^{--}\big\{C^{-}\{P\} \para  D^{-}\{Q\}\big\} \vspace{ 1.5mm}
\\
\rulename{r:IfTr} &
C\{\ifte{e}{P}{Q}\} \pired C\{P\}  \quad (e \downarrow \mathtt{true})  \vspace{ 1.5mm}
\\
 \rulename{r:IfFa} &
C\{\ifte{e}{P}{Q}\} \pired C\{Q\}  \quad (e \downarrow \mathtt{false}) \vspace{ 1.5mm}
\\

 \rulename{r:Str} &
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q \vspace{ 1.5mm}
\\
 \rulename{r:Par} & \text{if } P \pired P' ~~\text{then} ~~ P \para Q \pired P' \para Q  \vspace{ 1.5mm}
\\
 \rulename{r:Res} &
\text{if } P \pired P' ~~\text{then} ~~ \restr{\cha}{P} \pired \restr{\cha}{P'} %\vspace{2mm} \\

\end{array}
$$
}
\caption{Reduction semantics. } \label{tab:semantics}
\end{table}

In Table~\ref{tab:semantics}, duality for polarities $p$ is as expected: $\overline{+} = -$ and $\overline{-} = +$. 
We write $\pired^{*}$ for the reflexive, transitive closure of $\pired$.
As processes can be arbitrarily nested inside locations, 
reduction rules use  \emph{contexts}, i.e., processes with a \emph{hole} $\bullet$
\begin{definition}[Contexts]\label{d:context}
The set of \emph{contexts} is defined by the following syntax:
$$
C, D, E, \ldots ::= \{\bullet\} \sepr \component{l}{h}{\Delta}{C \para  P} %\sepr  \sepr \restr{\kappa}{C}  
$$
\end{definition}

%\jp{Why don't we have channel restriction in the syntax of contexts?}
This way, given a context $C\{\bullet\}$ and a process $P$, 
we write $C\{P\}$ to denote the process obtained by filling in the holes in $C$ with $P$.
The intention is that $P$ may reduce inside $C$, thus reflecting the transparent containment realized by location nesting.
We assume the expected extension of $\equiv$ to contexts; in particular, we tacitly use $\equiv$ to enlarge the scope of restricted channels in contexts as needed.
As mentioned above, reduction relies on located processes with annotations $h$, which denote the number of active sessions at every location.
To ensure the coherence of such annotations along reduction, 
 we define operations over contexts
 which allow us to increase/de\-crease the annotation $h$ on every location contained in a context. 
 
 \begin{definition}[Operations over contexts] 
Given a context $C$ as in Def.~\ref{d:context}, an integer $j$,
and an operator $* \in \{+,-\}$, %and $ \otimes \in \{\addelta, \midelta \}$, 
we define $C^{*j}$ as follows: 
$$ (\{\bullet\})^{*j}_{}  = \bullet \qquad~~ (\component{l}{h}{\Delta}{C \para P})^{*j}_{} = \component{l}{{h*j}}{\Delta}{C^{*j}_{} \para P} %\quad~~ (C \para  P)^{*j}_{} = C^{*j}_{} \para  P 
$$
\end{definition}

This way, e.g., ${C}^{+1}$ 
denotes the context $C$ in which 
 the runtime annotations for all locations have been incremented by one.
We  write ${C}^{-}$, ${C}^{+}$, ${C}^{--}$, and ${C}^{++}$ to stand for ${C}^{-1}$, ~${C}^{+1}$, ${C}^{-2}$, and ${C}^{+2}$, respectively.


We now comment on rules \rulename{r:Open}, \rulename{r:Upd}, \rulename{r:Pass}, and \rulename{r:Close} in Table~\ref{tab:semantics}; 
other rules are either standard or self-explanatory.
Rule \rulename{r:Open} formalizes session establishment. There are three distinguished contexts: while $C$ contains the (linear) service offer and 
$D$ encloses the service request, context $E$ encloses both $C$ and $D$. 
By matching on name $a$ a session is established; 
following~\cite{DBLP:journals/acta/GayH05,DBLP:journals/entcs/YoshidaV07}, 
this is realized by endowing each partner with a fresh polarized channel (or end-point) $\kappa^p$.
As such, channels $\kappa^+$ and $\kappa^-$ are runtime entities. 
%with a fresh channel $c$; \jp{This is the point where we should explain runtime $\kappa$} at runtime, each process gets one end of the channel.
Because of session initiation, the number of active sessions 
should be increased across all enclosing contexts: we increment by one in contexts $C$ and $D$ and by two in context $E$, for it encloses both endpoints. 
This increment realizes a form of protection against update actions; observe that due to the  transparency of locations, any updates may take place independently from the actual nested structure.
The reasons for the increment should be clear from rule \rulename{r:Upd}, which formalizes the update/reconfiguration of a location $l$, 
enclosed in contexts $C$ and $E$.  
Notice how the update action can only occur if the number of open (active) sessions in $l$ is 0.
By forcing updates to occur only when any (located) session behavior has completed (cf. rule \rulename{r:Close}), reduction ensures that 
active sessions are not inadvertently disrupted. %update actions which may interrupt session communications.
When possible, an update action  is then realized by 
  substituting $Q$ (the current behavior of $l$) into  $P(\mathsf{X})$. Informally, it is the adaptation mechanism who ``moves'' to realize reconfiguration. This is a form of \emph{objective update}, as the located process does not 
contain information on future update actions: it reduces autonomously until it is adapted by an  update process in its surrounding context. 
Rule \rulename{r:Pass} is the standard rule for delegation; in our setting, endpoint mobility is reflected by appropriate decrements/increments in the contexts enclosing the session sender/receiver. 
Rule \rulename{r:Close} formalizes the synchronized session closure. In analogy with rule \rulename{r:Open}, session closure 
should decrease the active session annotation in all enclosing contexts.
%\jp{We no longer need to refer to interfaces here, only to the fact that runtime annotation $h$ is used to avoid inconsistent updates}
%Let us write $\intf{P}$ for the \emph{interface} of process $P$ (cf. Sect.~\ref{s:types}). 

\subsection{Examples of Runtime Adaptation}\label{ss:examp}

%\begin{example}
%In order to illustrate the syntax and semantics of our framework, 
We now present 
some patterns of runtime adaptation that can be expressed in our process framework.
Recall that $l_1, l_2, \ldots$ denote identifiers for locations.

%We give here some examples on how adaptable processes can be used:
 \begin{description}
 \item[Relocation.] One of the simplest reconfiguration actions that 
 can be represented in our model is the relocation of an arbitrary behavior %at a location 
 to a completely different
 computation site. 
 The following reduction illustrates how a synchronization on location $l_1$ leads to 
 a relocation from $l_1$ to $l_2$:
% Similarly, one can think of moving the content of a locality $a$ into a fresh locality $b$:
$$\bigcomponent{l_1}{0}{}{\,\compo{l_4}{0}{Q}\,} \para \adaptn{l_1}{\compo{l_2}{}{ \mathsf{X} }} \pired \bigcomponent{l_2}{0}{}{\,\compo{l_4}{0}{Q}\,} \para \nil $$

 
\item[Deep Update.] 
Because our locations are transparent, an update action may have influence on located processes not necessarily at top-level
in the nested process structure. 
The reduction below illustrates how the influence of an update process on name $l_3$ can cross locations $l_1$ and $l_2$ in order
to realize an adaptation routine, represented by process $S'$:
%We start with an example that underlines the transparency of adaptable processes, here we are going to substitute the adaptable process located at $c$ with a new adaptable process $S'$ located inside $d$. Notice that $c$ occurs inside $b$ that is on its turn inside $a$. Thus:
$$\bigcomponent{l_1}{0}{}{Q \para \bigcomponent{l_2}{0}{}{R \para \compo{l_3}{0}{S_{1}} }\,} \para 
\adaptn{l_3}{\compo{l_4}{}{S'(\mathsf{X})}} 
\pired 
\bigcomponent{l_1}{0}{}{Q \para \compo{l_2}{0}{R \para \compo{l_4}{0}{S_{2}}\, }\, } \para \nil $$
where $S_2 = S'\sub{S_1}{\mathsf{X}}$.
That is, by virtue of the update action on $l_3$, its current behavior  (denoted $S_1$) is suspended 
and possibly used in the new behavior $S'$, which is now located at $l_4$.

 \item[Upgrade.] Interestingly, update actions do not need to preserve the current behavior at a given location. 
 In fact, if the adaptation routine embodied by the updated process does not contain a process variable, 
 then the current behavior at the location will be discarded.
 This feature is illustrated by the following reduction, in which we assume that $\mathsf{X} \notin \mathsf{fv}(Q)$:
 % Next, we show how to destroy locality $a$ and its content. In this case we require $\mathsf{X} \notin \mathsf{fv}(Q)$, this way $Q$ is a closed process and $Q\sub{P}{\mathsf{X}}= Q$ thus obtaining:
$$ \compo{l_1}{0}{P} \para \adapt{l_1}{Q}{X} \pired Q \para \nil $$
Observe that the location on which the update action takes place does not need to be preserved either:
had we wanted to only replace the behavior at $l_1$, then it suffices to enclose 
the runtime adaptation code $Q$ within a located process named $l_1$, i.e.,
%recreate the locality $a$ in the update construct:  
$\adaptn{l_1}{\compo{l_1}{}{Q(\mathsf{X})}}$. 


\item[Conditional Backup.]   The current behavior of a location may be used more than once by an
adaptation routine.
Consider process $B_e$ below:
$$
B_e = \compo{l_1}{0}{Q} \para \bigcomponent{l_5}{0}{}{\,
\ifte{e}{\adaptn{l_1}{\compo{l_2}{}{\mathsf{X}}}}{\adaptn{l_1}{\compo{l_1}{}{\mathsf{X}} \para \compo{l_3}{}{\mathsf{X}}}}\,}
$$
Depending on the boolean expression $e$ reduces to, 
$B_e$ may either (i) simply relocate the behavior at $l_1$, 
or (ii) define a ``backup copy''  of $Q$ at  $l_3$: %. More precisely:
\begin{eqnarray*}
B_e & \pired^* & \compo{l_2}{0}{Q} \para \compo{l_5}{0}{\nil} \quad \qquad \qquad\text{if $e \downarrow \mathtt{true}$} \\
B_e & \pired^* & \compo{l_1}{0}{Q} \para \compo{l_3}{0}{Q} \para \compo{l_5}{0}{\nil} \qquad\text{if $e \downarrow \mathtt{false}$}
\end{eqnarray*}
\end{description}

\noindent
The above examples are useful to illustrate the expressiveness of adaptable processes for representing 
rich  adaptation mechanisms. As our process model includes both communication and update actions,
we require mechanisms for harmonizing both kinds of actions, avoiding undesirable disruptions of communication behavior by updates.
In the next section, we define a static analysis technique that forces update actions to be enabled only when 
there are no active communication behaviors.



% 
 \section{The Type System}\label{s:types}
Our type discipline builds upon the one given in~\cite{DBLP:journals/entcs/YoshidaV07},
extending it so as to account for disciplined runtime adaptation.
%\cite{DBLP:conf/ppdp/GarraldaCD06}.
%As mentioned in the Introduction, a 
A
main criteria in the design of our type discipline is \emph{conservativity}:
we would like to enforce both disciplined communication and disciplined adaptation by preserving as much as possible standard models of session types.
Thus, our type syntax (given below) is rather standard; also, we rely on a typing judgment which extends usual notions with an  \emph{interface}~$\INT$. Intuitively, interfaces describe the services declared in a given process.
%Our type syntax is as follows: %defined next, contains the usual session types constructs: %---we exclude recursive types.

%As such, the type syntax is divided into three categories: \emph{basic types}, which  handle expressions; 
%\emph{pre-session types} describing a channel's ability for sending/receiving messages and offering/selecting be\-hav\-iors; 
%\emph{session types} representing well-formed session-typed be\-hav\-ior. %; and
%\emph{channel types}, which can be a session type or a \emph{used session}~$\bot$. %this will be made clear later on).

%We extend the judgments of~\cite{DBLP:conf/ppdp/GarraldaCD06} with an \emph{interface} $\INT$---the collection of all session types declared in a given process. 
%
%Formally, we have:

%\end{document}
 
\begin{definition}[Types]\label{d:types}
The syntax of 
 \emph{basic types} (ranged over $\capab, \sigma,   \ldots$) %, \emph{pre-session types} ($\zeta$), 
 and
 %(qualified) 
 \emph{session types} (ranged over $\ST, \beta, \ldots$)
% and \emph{channel types} ($\omega$) 
is given in Table~\ref{tab:types}.
\end{definition}

\begin{table}[t]
\textsc{Types}
$$
\begin{array}{lclr}
\capab, \sigma & ::= & \mathsf{int} \sepr \mathsf{bool} \sepr \dots ~~~& \text{basic types}\\

\alpha, \beta &::=  &  !(\tilde{\capab}).\alpha \sepr ?(\tilde{\capab}).\alpha & \text{send, receive} \\ 
		& \sepr &  !(\beta).\alpha \sepr ?(\beta).\alpha & \text{throw, catch} \\ 
		& \sepr &  \&\{n_1:\alpha_1, \dots,  n_m:\ST_m \}  \quad &  \text{branch} \\
		& \sepr &  \oplus\{n_1:\alpha_1, \dots , n_m:\ST_m \}  &  \text{select} \vspace{0.5mm} \\
		& \sepr &  \epsilon \!\!\!\!\!\!& \text{closed session}
\end{array}
$$
\textsc{Environments}
$$
\begin{array}{lclr}
		\qua & ::= &  \qual \sepr \quau  & \text{type qualifiers} \vspace{0.5mm} \\
\INT &::= &  \emptyset \sepr \INT, \langle a: \ST, h \rangle & \text{interface} \\
\ActS & ::= &  \emptyset \sepr \ActS , k:\ST \sepr \ActS ,  [k:\ST]  & \text{typing with active sessions}\\
\Gamma &::= &  \emptyset \sepr \Gamma, e:\capab \sepr \Gamma, a:\langle \ST_\qua , \overline{\ST_\qua} \rangle \quad& \text{first-order environment}\\
\Theta &::= &  \emptyset \sepr  \Theta,\mathsf{X}:\INT \sepr \Theta,l:\INT     \quad& \text{higher-order environment}
\end{array}
$$  
\caption{Types and Typing Environments}\label{tab:types}
\end{table}



% We use $t, t', \ldots$ to range over \emph{type variables}; also, we 
% require recursive types to be \emph{contractive}, i.e., not 
% containing a subexpression of the form $\mu t.\mu t_1.\cdots.\mu t_n.t$.
% Binder $\mu$ gives rises to standard notions of free/bound type variables; 
% $\mathsf{ftv}(\zeta)$ denotes the free type variables in $\zeta$.
% We consider session types modulo folding/unfolding of recursive types.
%\todo{contractive types?}
We recall the intuitive meaning of session types. 
Type $?(\tilde{\capab}).\ST$ (resp. $?(\beta).\ST$) abstracts the behavior of a channel 
which receives values of types $\tilde{\capab}$ (resp. a channel of type $\beta$) 
and continues as $\ST$ afterwards.
In a complementary way, type $!(\tilde{\capab}).\ST$ (resp. $!(\beta).\ST$) represents the behavior
of a channel which sends values (resp. a channel)  and that continues as $\ST$ afterwards.
Type $\&\{n_1:\alpha_1, \dots,  n_m:\ST_m \}$ describes a branching behavior, or external choice, along a channel:
it offers $m$ behaviors, and if the $j$-th alternative is selected then it behaves as described by type $\ST_j$ ($1 \leq j \leq m$).
In turn, type $\oplus\{n_1:\alpha_1, \dots , n_m:\ST_m \}$ describes the behavior of a channel which 
may select a single behavior among  $\alpha_1, \ldots, \alpha_m$. This is an internal choice, which continues as $\ST_j$ afterwards.
Finally, type $\epsilon$ represents a channel with no communication behavior. 
We now introduce the central notion of  \emph{duality} for (session) types.


\begin{definition}[Duality]\label{d:dual}
Given a session type $\ST$, 
its \emph{dual}
(noted $\overline{\ST}$) is inductively defined in Table~\ref{tab:dual}.
\begin{table}[t]
$$
\begin{array}{rcl}
 \overline{\epsilon} & =  & \epsilon\\
 \overline{!(\tilde{\capab}).\ST} & =  & ?(\tilde{\capab}).\overline{\ST} \\
 \overline{?(\tilde{\capab}).\ST} & =  & !(\tilde{\capab}).\overline{\ST} \\
 \overline{!(\beta).\ST} & =  & ?(\beta).\overline{\ST} \\
 \overline{?(\beta).\ST} & =  & !(\beta).\overline{\ST} \\
% \overline{t} &\!\!=\! & t \\
 %\overline{\mu t.\ST} &\!\!=\! & \mu t.\overline{\ST}\\
 \overline{\&\{n_1:\ST_1 , \ldots , n_m:\ST_m \}} &\!\!=\! & \oplus\{n_1:\overline{\ST_1} , \ldots , n_m:\overline{\ST_m} \}\\
 \overline{ \oplus\{n_1:\ST_1 , \ldots , n_m:\ST_m \}} &\!\!=\!& \&\{n_1:\overline{\ST_1} , \ldots , n_m:\overline{\ST_m} \}
\end{array}
$$ %\vspace{-4mm}
\caption{Dual of session types}\label{tab:dual}
\end{table}
\end{definition}

Before introducing our notions of typing environments, we formally define the concept of interface, motivated above.

\begin{definition}[Interfaces]\label{d:interf}
An \emph{interface} $\INT$ is a set of pairs  $\langle a: \ST, h\rangle$ where 
$a$ is name, $\ST$ is a session type, and either $h> 0$ or $h = \infty$.
The extension of an interface $\INT$ with a pair $\langle a: \ST, h\rangle$, written $\INT \addelta \inter{a}{\alpha}{h}$,
is defined as follows:
$$
\INT \addelta \inter{a}{\alpha}{h} \triangleq
\begin{cases}
\INT' \cup \{\inter{a}{\ST}{h + j} \} & \text{if } \exists\INT'. \,  \INT = \INT' \cup \{\inter{a}{\ST}{j} \}	\\
\INT \cup \{\inter{a}{\ST}{h}\} & \text{otherwise} 
\end{cases}
$$
Given $\INT$, we write $\INT_\quau$ 
and $\INT_\qual$
to denote sets $\{ \inter{a}{\ST}{h} \,|\, \inter{a}{\ST}{h} \in \INT \land h = \infty\}$ and
$\INT - \INT_\quau$, respectively. \\
Moreover, we write $\INT \unres$ 
to denote the set $\{ \inter{a}{\alpha}{\infty} \mid   \inter{a}{\alpha}{h} \in \INT_\qual \} \cup \INT_\quau$.
%Finally we define the  function $$\unres(\INT) \triangleq \{ \inter{a}{\alpha}{\infty} \mid   \inter{a}{\alpha}{h} \in \INT \}$$
\end{definition}


We recall that $\infty + 1 = \infty$.
Intuitively, interfaces capture the services declared in a process (i.e., an assignment from names to session types)
together with
the number of times such a service is declared ($j>0$ if a type is linear; $\infty$ otherwise).
In $\INT$, services are recorded at most once; several occurrences of the same linear service are captured
by the second component of the pair.   
We sometimes write $\INT \addelta a:\ST_\qual$ 
and  $\INT \addelta a:\ST_\quau$
to stand 
for $\INT \addelta\{\inter{a}{\ST}{1} \}$ and 
$\INT \addelta \{\inter{a}{\ST}{\infty} \}$, respectively.
The extension of $\addelta$ from single pairs $\inter{a}{\ST}{h}$ 
to interfaces, denoted $\INT_1 \addelta \INT_2$, is as expected. 

It is useful to relate different interfaces. % which only differ in the linear services they contain.
This is the intention of the 
relation $\intpr$ over interfaces, defined next.

\begin{definition}[Interface Ordering] \label{d:intpre}Given interfaces $\INT$ and $\INT'$, we write 
$\INT  \intpr \INT'$ iff 
\begin{enumerate}[1.]
\item $\INT_\quau \subseteq \INT'_\quau$.
\item $\forall \inter{a}{\alpha}{h} \in \INT_\qual $  then 
$ \inter{a}{\alpha}{h'} \in \INT'_\qual $, for some $h'$ such that $h \leq h'$
\end{enumerate}
\end{definition}

\begin{lemma}
Relation \intpr is a preorder.
\end{lemma}

As we will see, our typing system will be parametric on the definition of \intpr.
Alternative definitions for this relation are discussed in Sect.~\ref{sec:int}.

The typing environments we rely on are defined in the lower part of Table~\ref{tab:types}.
In addition to interfaces $\INT$, we consider typings $\ActS$ and environments $\Gamma$ and $\Theta$.
As typical in session types disciplines, 
typing $\ActS$ collects 
assignments from channels to session types, therefore describing 
currently active sessions. 
Unlike usual disciplines, however, in $\ActS$ we also include \emph{bracketed assignments}, denoted $[\kappa^p:\ST]$,
which represent active but restricted sessions. 
As we discuss below, bracketed assignments arise in the typing of channel restriction, 
and are key to keep a precise count of the active sessions in a given location. 
We write $dom(\ActS)$ to denote the set $\{ \cha^p \mid \cha^p:\ST \in \ActS \lor [\cha^p:\ST] \in \ActS\}$.
$\Gamma$ is a first-order environment which maps expressions to basic types
and names to pairs of \emph{qualified} session types.
Within the interface, session types can be linear ($\qual$) or unrestricted ($\quau$). 
While $\qual$ is used for those session types to be used just once, 
$\quau$ qualifies those session types intended to feature a persistent behavior.
The higher-order environment $\Theta$ 
collects assignments of process variables and locations to interfaces. 
While the former kind of assignments is relevant to update processes, the latter concern located processes.
As we explain next, by relying on the combination of these two pieces of information the type system ensures that
runtime adaptation actions preserve the behavioral interfaces of a process.
%\jp{The following is a bit strange for locations are also in $\T$; I would write $vdom(\T)$ if you only care about variables.} \todo{
We write $vdom(\Theta)= \{ \mathsf{X} \mid \mathsf{X}:\INT \in \Theta \}$ to denote the variables in the domain of $\Theta$.
%}
Given these environments, a \emph{type judgment} is  of form
$$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} $$ 
meaning that, under environments $\Gamma$ and $\Theta$, 
process $P$ has active sessions declared in $\ActS$ and interface 
$\INT$. We then have:

\begin{definition}%[Well-typed process]
A process is well-typed if it can be typed using the rules in Tables~\ref{tab:ts} and~\ref{tab:session}.


\begin{table}[th!]
$$
\begin{array}{c}
% \mathrm{\textsc{Comp}}~~~\component{a}{P} \arro{~\component{a}{P}~}  \star
\infer[\rulename{t:Exp}]{\Gamma \vdash e:\capab}{} \ \
\infer[\rulename{t:NVar}]{\Gamma, x:\capab \vdash x:\capab}{} \ \ 
\infer[\rulename{t:Nil}]{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}{}
\\ \\
 \infer[\rulename{t:LocEnv}]{\Theta, l:\INT \vdash l:\INT}{} \quad
\infer[\rulename{t:PVar}]{\Gamma; \Theta,\mathsf{X}:\INT \vdash \mathsf{X}:\type{\emptyset}{\INT}}{}
\\
\\
 \infer[\rulename{t:Accept}]{\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P}{ \type{\ActS}{\,\INT \addelta a: \ST_\qual}}}{
\Gamma \vdash a: \langle \ST_\qual , \overline{\ST_\qual } \rangle \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\ST}{\,\INT}} 
} 
\\
\\
 \infer[\rulename{t:RepAccept}]{\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P}{ \type{\emptyset}{\INT\unres \addelta \, a: \ST_\quau}}}
 {
\Gamma \vdash a: \langle \ST_\quau , \overline{\ST_\qual } \rangle \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{x:\ST}{\,\INT}} 
}
\\
\\
 \infer[\rulename{t:Request}]{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{x}.P}{ \type{\ActS}{\,\INT \addelta a: \overline{\ST_\qual }}}} 
 {
\Gamma \vdash a: \langle \ST_\qua , \overline{\ST_\qual} \rangle \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\overline{\ST }}{\,\INT}} 
}
\\
\\
 \infer[\rulename{t:Clo}]{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\epsilon}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \qquad k\notin \dom{\ActS} }
 \\ \\
 \infer[\rulename{t:Loc} ]{\judgebis{\env{\Gamma}{\Theta}}{\component{l}{h}{\INT}{P} }{ \type{\ActS}{\INT' }}}
 {
       \Theta \vdash l:\INT \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } } \qquad  h = | \ActS |  \qquad \INT' \intpr \INT
 }
 \\
\\
 \infer[\rulename{t:Adapt} ]{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{X}}{\type{\emptyset}{ \emptyset}}} 
{\Theta \vdash l:\INT  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT}}}{P}{\type{\emptyset}{ \INT' }}}
\\
 \\
 \infer[\rulename{t:CRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT}}}
 \\
\\
 \infer[\rulename{t:Par}]{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT_1 \addelta \INT_2}}}
 {
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \qquad
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
 }
 \end{array}
 $$
\caption{Well-typed processes (I)} \label{tab:ts}
\end{table}
\end{definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\begin{table}[!t]
%$$
%\begin{array}{cr}
%\cfrac{}{\Gamma \vdash e:\capab} \qquad 
%\cfrac{}{\Gamma, x:\capab \vdash x:\capab}  \qquad
%\cfrac{}{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}} 
% & \rulename{t:Exp},  \rulename{t:NVar}, \rulename{t:Nil} \\
%
%\cfrac{}{\Theta, l:\INT \vdash l:\INT}
%\quad \cfrac{}{\Gamma; \Theta,\mathsf{X}:\INT \vdash \mathsf{X}:\type{\emptyset}{\INT}}
%&    \rulename{t:LocEnv},  \rulename{t:PVar}   \vspace{2mm}\\
%
% \cfrac{
%\Gamma \vdash a: \langle \ST_\qual , \overline{\ST_\qual } \rangle \qquad
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\ST}{\,\INT}} 
%}{\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P}{ \type{\ActS}{\,\INT \addelta a: \ST_\qual}}} 
%& 
%\rulename{t:Accept} \vspace{2mm} 
%\\
%
% \cfrac{
%\Gamma \vdash a: \langle \ST_\quau , \overline{\ST_\qual } \rangle \qquad
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{x:\ST}{\,\INT}} 
%}{\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P}{ \type{\emptyset}{\INT\unres \addelta \, a: \ST_\quau}}} 
%& 
%\rulename{t:RepAccept} \vspace{2mm} 
%\\
%
%% \cfrac{
%%\Gamma \vdash a: \langle \ST_\quau , \overline{\ST_\qual } \rangle \quad
%%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{x:\ST}{\,\todo{$\INT_\quau$}}} 
%%}{\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P}{ \type{\emptyset}{\INT_\quau \addelta \, a: \ST_\quau}}} 
%%& 
%%\rulename{t:RepAcceptProp} \vspace{2mm} 
%%\\
%
%\cfrac{
%\Gamma \vdash a: \langle \ST_\qua , \overline{\ST_\qual} \rangle \qquad
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\overline{\ST }}{\,\INT}} 
%}{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{x}.P}{ \type{\ActS}{\,\INT \addelta a: \overline{\ST_\qual }}}} 
%& 
%\rulename{t:Request} \vspace{2mm} 
%\\
% \cfrac{\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \qquad k\notin \dom{\ActS} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\epsilon}{ \INT}}} & \rulename{t:Clo} \vspace{2mm} \\
%
%\cfrac{
%       \Theta \vdash l:\INT \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } } \qquad  h = | \ActS |  \qquad \INT' \intpr \INT
% }{\judgebis{\env{\Gamma}{\Theta}}{\component{l}{h}{\INT}{P} }{ \type{\ActS}{\INT' }}} &  \rulename{t:Loc}  \vspace{2mm}
%\\
%
%
%\cfrac{\Theta \vdash l:\INT  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT}}}{P}{\type{\emptyset}{ \INT' }}}{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{X}}{\type{\emptyset}{ \emptyset}}} & \rulename{t:Adapt}  \vspace{2mm}
%
%\\
% 
%\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT}}} 
%& \rulename{t:CRes} 
%\vspace{2mm}
%
%\\
%\cfrac{
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \qquad
% \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
% \qquad
% \INT = \INT_1 \addelta \INT_2}{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT}}} & \rulename{t:Par}  
%\end{array}
%$$
%\caption{Well-typed processes (I)} \label{tab:ts}
%\end{table}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{table}[th!]
$$
\begin{array}{c}
\infer[\rulename{t:Thr}]{\judgebis{\env{\Gamma}{\Theta}}{\throw{k}{k'}.P}{\type{\ActS, k:!(\ST).\STT, k':\ST}{ \INT}}} 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT}{ \INT}}}
\\  
\\
\infer[\rulename{t:Cat}]{\judgebis{\env{\Gamma}{\Theta}}{\catch{k}{x}.P }{\type{\ActS, k:?(\ST).\STT}{ \INT}}}
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT, x:\ST}{\INT}}}
\\
\\
\infer[\rulename{t:In}]{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{\tilde{x}}.P }{\type{\ActS, k:?(\tilde{\capab}).\ST}{ \INT}}}
{\judgebis{\env{\Gamma, \tilde{x}:\tilde{\capab}}{\Theta}}{P}{\type{\ActS, k:\ST}{\INT}}}
\\
\\
\infer[\rulename{t:Out}]{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{\tilde{e}}.P}{\type{\ActS, k:!(\tilde{\capab}).\ST}{ \INT}}}
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST}{ \INT}} \quad \Gamma \vdash \tilde{e}:\tilde{\capab}}
\\
\\
\infer[\rulename{t:Weak}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT }}} 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \qquad \cha^+, \cha^- \notin dom(\ActS)}
\\
\\ 
\infer[\rulename{t:If}]{\judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{\type{\ActS}{\INT}}} 
 {
 \Gamma \vdash e:\mathsf{bool} \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} \qquad
\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}
 }
 \\
  \\
\infer[\rulename{t:Bra}]{\judgebis{\env{\Gamma}{\Theta}}{\branch{k}{n_1{:}P_1 \! \parallel \!\ldots \!\parallel n_m{:}P_m}}{\type{ \ActS, k:\&\{n_1{:}\ST_1, \ldots, n_k{:}\ST_m \}}{\INT}}} 
{
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS, k:\ST_1}{ \INT}} 
\ 
\cdots
\
\judgebis{\env{\Gamma}{\Theta}}{P_m}{\type{\ActS, k:\ST_m}{ \INT}} %\qquad \rulename{t:Bra}
 }
 \\
\\
\infer[\rulename{t:Sel}]{\judgebis{\env{\Gamma}{\Theta}}{\select{k}{n_i};P}{\type{\ActS, k:\oplus\{n_1:\ST_1, \ldots,  n_m:\ST_m \}}{\INT}}}
{
\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST_i}{ \INT}} \qquad 1 \leq i \leq m 
} 
\end{array}
$$% \vspace{-4mm}
\caption{Well-typed processes (II)}\label{tab:session}
\end{table}




We comment on some non standard rules in Table~\ref{tab:ts}.
Given a process which implements session type $\ST$  on channel $x$, 
rule \rulename{t:Accept} types linear service acceptance processes on name $a$. 
Observe how $x$ is removed from $\ActS$ whereas
 $\INT$ is appropriately extended with $a : \ST_\qual$. Rule \rulename{t:RepAccept} is its analogous in an unrestricted setting.
In that rule, observe how the linear services in  $\INT$ are ``promoted'' to unrestricted services via $\INT\unres$ (cf. Def.~\ref{d:interf}).
%\todo{
Linear services that appear in the context of a persistent service $a$ are meant to be executed exactly once for each copy of $a$. 
In fact, after promotion the declaration in $\Gamma$ for a linear service $b:\langle \ST_{\qual}, \overline{\ST_{\qual}} \rangle$ remains unchanged, but its entry in $\INT$ should be $\inter{b}{\ST}{\infty}$, as we could now observe an unbounded number of linear executions of $b$.
%}
%\jp{Cinzia, please check I didn't modified the intended meaning of your text.}
Given these typing rules, rule \rulename{t:Request} should be self-explanatory.
Rule \rulename{t:CRes} types channel restriction. 
The main difference wrt usual typing rules for channel restriction (cf.~\cite{DBLP:journals/entcs/YoshidaV07}) is that 
restricted end-points are not removed from $\ActS$ but kept in bracketed form. 
This allows us to use typing $\ActS$ to have an exact count of open, possibly restricted, sessions in a process.
Rule \rulename{t:Close} types the explicit session closure construct, extending 
$\ActS$ with a fresh channel which is assigned to an empty session type. 
This may be useful to understand why our typing rule for the inactive process (rule \rulename{t:Nil})
requires an empty typing $\Delta$.
%\jp{Far notare la nostra regola Rule \rulename{t:Nil} inizia da un $\Delta$ vuoto...}
Rule \rulename{t:Loc} performs two checks to type located processes. First, the runtime annotation 
$h$ is computed by counting the assignments (standard and bracketed) declared in $\ActS$.
Second, the rule checks that the interface of the located process is less  or equal (in the sense of $\intpr$, cf. Def.~\ref{d:intpre}) than the
declared interface of the given location. 
Informally, this ensures that the process behavior does not ``exceed'' the expected behavior within the location.
It is worth observing how a typed located processes has the exact same typing and interface of its contained process:
this is how transparency of locations arises in typing.
Finally, rule \rulename{t:Adapt} types update processes. Observe how the interface associated to the process variable of the given 
 adaptation routine should match with the declared interfaces for the given location. 
However, for simplicity we establish no condition on the relation between $\INT$ (the expected interface) 
and $\INT'$ (the interface of the adaptation routine $P(\mathsf{X})$)---Sect.~\ref{sec:int} discusses an alternative formulation.

% 
 \section{Session Safety and Consistency by Typing}\label{sec:res}
Here we investigate \emph{safety} and \emph{consistency}, the main properties of our typing system.
While safety (discussed in Sect.~\ref{ss:safety}) corresponds to the expected guarantee of adherence to prescribed session types and absence of runtime errors, 
consistency (discussed in Sect.~\ref{ss:consist})  formalizes a correct interplay between communication actions and update actions.
Defining both properties requires the following notions of \emph{$\kappa$-processes}, \emph{$\kappa$-redexes}, 
and \emph{error process}.
These are classic ingredients in session types presentations (see, e.g., \cite{DBLP:conf/esop/HondaVK98,DBLP:journals/entcs/YoshidaV07});
our notions generalize usual definitions 
to the case in which processes which may interact even if contained in arbitrarily nested transparent locations (formalized by the contexts of 
Def.~\ref{d:context}).

\begin{definition}[$\kappa$-processes, $\kappa$-redexes, errors]\label{d:kred}
A process $P$ is a \emph{$\kappa$-process} if it is a prefixed process with subject $\kappa$, i.e., 
$P$ is one of the following:
$$
%\begin{array}{llcllcrl}
%  &  \inC{\kappa^{\,p}}{\tilde{x}}.P' & &  & \outC{\kappa^{\,p}}{v}.P' & &    &  \close{\kappa^{\,p}}.P'  \\
%  &   \catch{\kappa^{\,p}}{x}.P' & &  &    \throw{\kappa^{\,p}}{d^{\,q}}.P' \\
%  &   \branch{\kappa^{\,p}}{n_1{:}P_1 \parallel \ldots \parallel n_m{:}P_m} ~~ & &  &   \select{\kappa^{\,p}}{n}.P' 
%\end{array}
\begin{array}{ll}
    \inC{\kappa^{\,p}}{\tilde{x}}.P' & \outC{\kappa^{\,p}}{v}.P'    \\
  \catch{\kappa^{\,p}}{x}.P' &  \throw{\kappa^{\,p}}{k^{\,q}}.P' \\
   \branch{\kappa^{\,p}}{n_1{:}P_1 \parallel \ldots \parallel n_m{:}P_m}  &   \select{\kappa^{\,p}}{n}.P' \\
    \close{\kappa^{\,p}}.P' & 
\end{array}
$$
Process $P$ is a \emph{$\kappa$-redex} if 
it contains the composition of exactly two $\kappa$-processes with opposing polarities, i.e., 
for some contexts $C$, $D$, and $E$,
$P$ is 
structurally congruent to
one of the following:
$$
\begin{array}{c}
(\nu \tilde{\kappa})(E\big\{C\{\inC{\kappa^{\,p}}{\tilde{x}}.P_1\} \para D\{\outC{\kappa^{\,\overline{p}}}{v}.P_2\}\big\}  )\\  
(\nu \tilde{\kappa})(E\big\{C\{\catch{\kappa^{\,p}}{x}.P_1\} \para  D\{\throw{\kappa^{\,\overline{p}}}{k^{\,q}}.P_2\} \big\}) \\
(\nu \tilde{\kappa})(E\big\{C\{\branch{\kappa^{\,p}}{n_1{:}P_1 \parallel \ldots \parallel n_m{:}P_m} \} \para  D\{  \select{\kappa^{\,\overline{p}}}{n_i};P'\}\big\} )  \\
(\nu \tilde{\kappa})(E\big\{C\{\close{\kappa^{\,p}}.P_1\}  \para  D\{\close{\kappa^{\,\overline{p}}}.P_2\}\big\})
\end{array}
$$
We say a $\kappa$-redex is \emph{located} if one or both of its $\kappa$-processes is inside at least one located process.

$P$ is an \emph{error} if
$P \equiv (\nu \tilde{\kappa})(Q \para R)$
where, for some $\kappa$, $Q$ contains 
\underline{either} 
%exactly one $\kappa$-process
%\underline{or}
exactly 
two $\kappa$-processes that do not form a $\kappa$-redex
\underline{or}
three or more $\kappa$-processes.
\end{definition}




\subsection{Session Safety}\label{ss:safety}


We now give
subject congruence and subject reduction results for our typing discipline.
Together with some 
some auxiliary results, these provide the basis for the proof of type safety (Theorem~\ref{t:safety} in Page~\pageref{t:safety}).
We start by giving three standard results, namely weakening, strengthening, and channel lemmas.


\begin{lemma}[Weakening]
 Let $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$.  If $\mathsf{X} \notin vdom(\Theta)$ then $\judgebis{\env{\Gamma}{ \Theta,\mathsf{X}:\INT'}}{P}{\type{\ActS}{\INT}}$.
\end{lemma}
\begin{proof}
 Easily shown by induction on the structure of $P$.
\end{proof}


\begin{lemma}[Strengthening]
 Let $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$.
If $\mathsf{X}  \notin \mathsf{fv}(P)$ then $\judgebis{\env{\Gamma}{ \Theta \setminus \mathsf{X}:\INT'}}{P}{\type{\ActS}{\INT}}$.
\end{lemma}
\begin{proof}
 Easily shown by induction on the structure of $P$.
\end{proof}



\begin{lemma}[Channel Lemma]\label{lem:channel}
  Let $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$, 
 $\cha \notin \mathsf{fc}(P) \cup \mathsf{bc}(P)$ iff $\cha \notin dom(\ActS)$.
\end{lemma}
\begin{proof}
 Easily shown by induction on the structure of $P$.
\end{proof}

We are ready to show the Subject Congruence Theorem:

\begin{theorem}[Subject Congruence] \label{th:congr}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ and $P \equiv Q$ then $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}$.
\end{theorem}
\begin{proof}
By induction on the derivation of $P \equiv Q$, with a case analysis on the last applied rule.

%\begin{description}
\paragraph{\bf Case $\restr{\cha}{ ( \compo{l}{h}{P})  } \equiv   \compo{l}{h}{ \restr{\cha}{P}  }$} \quad \\
We examine the left to right direction:
we show that if 
$\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{ ( \compo{l}{h}{P} ) }}{\type{\ActS}{\INT}}$ 
then 
$\judgebis{\env{\Gamma}{\Theta}}{  \compo{l}{h}{\restr{\cha}{P}  }}{\type{\ActS}{\INT}}$.
Since $\restr{\cha}{  (\compo{l}{h}{P} ) }$ is well-typed, 
by inversion on rules \rulename{t:Loc} and \rulename{t:CRes}, 
for some $\ST, \Delta'$
we have:
$$
\cfrac{
\begin{array}{c}
\Theta \vdash l:\INT' \\
\INT \sqsubseteq \INT'
\end{array}
\quad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT} } \quad
 h = | \ActS', \cha^-:\ST, \cha^+:\overline{\ST} |  
}{\cfrac{\judgebis{\env{\Gamma}{\Theta}}{\compo{l}{h}{P} }{ \type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT}}} {\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{(\compo{l}{h}{P})}}{\type{\ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT }}}}
$$ 
%\jp{perhaps this is redundant:} 
Hence $ \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT}}$, 
where $\ActS = \ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]$.
Now, starting from $P$, and by applying first rule  \rulename{t:CRes} and then rule  \rulename{Loc} we obtain: 
$$
\cfrac
{
\cfrac{
 \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT} } 
}
{ 
\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT}}}
\ 
\begin{array}{c}
\Theta \vdash l:\INT' \qquad \INT \sqsubseteq \INT' \\
 h = | \ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]| 
\end{array}
}
{\judgebis{\env{\Gamma}{\Theta}}{\compo{l}{h}{\restr{\cha}{P}} }{ \type{\ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]}{\INT}}}
$$
Observe that 
$h = | \ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]| =  | \ActS', \cha^-:\ST, \cha^+:\overline{\ST}|$---bracketing does not influence $h$, i.e.,
The reasoning for the right to left direction is analogous and omitted.


\paragraph{\bf Case $P \para \nil  \equiv P $} \quad \\ 
We examine only the left to right direction; the converse direction is similar. 
We then show that if  $\judgebis{\env{\Gamma}{\Theta}}{P \para \nil }{\type{\ActS}{\INT}}$
then  $\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{\INT}}$.
 By inversion on rule \rulename{t:Par}  there exist $\Delta_1, \INT_1$ such that $$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{\INT_1}} \text{ and }  \judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}$$
with  $\ActS= \ActS_1 \cup \emptyset = \ActS_1$ and $\INT = \INT_1 \uplus \emptyset = \INT_1$ and so the thesis follows.




\paragraph{\bf Case $\restr{\cha}{P} \para Q \equiv \restr{\cha}{(P \para Q)}$ with $\cha \notin \mathsf{fc}(Q) $} \quad \\
We examine only the right to left direction; the other direction is analogous.
We show that if 
$\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{(P \para Q)}}{\type{\ActS}{\INT}}$ (with $\cha \notin \mathsf{fc}(Q)$) then 
also 
$\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{P \para Q}}{\type{\ActS}{\INT}}$.
By inversion on rules 
\rulename{t:CRes} and \rulename{t:Par}
we have:
$$
\cfrac{
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1,  \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT_1}} \qquad
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
 \qquad
 \INT = \INT_1 \addelta \INT_2}
{ \cfrac{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2, \cha^-:\ST, \cha^+:\overline{\ST} }{\INT'}}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{(P\para Q)}}{\type{\ActS_1 \cup \ActS_2, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT }}}}
$$
where $\ActS = \ActS_1 \cup \ActS_2, [\cha^-:\ST], [\cha^+:\overline{\ST}]$.
Observe how in the inversion of rule \rulename{t:Par} we have used assumption 
$\cha \notin \mathsf{fc}(Q) \cup \mathsf{bc}(Q)$  and Lemma \ref{lem:channel}  to infer 
$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1,  \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT_1}}$ and $ \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}$. Now, % and we can construct the following derivation tree
using first rule  \rulename{t:CRes} and then rule  \rulename{t:Par} we have:
 $$
\cfrac{ 
\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1,  \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT_1}}}
{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS_1, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT_1 }}}
\quad 
\begin{array}{c}
\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
\\
 \INT = \INT_1 \addelta \INT_2
\end{array}
 } 
{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}\para Q}{\type{\ActS_1 \cup \ActS_2, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT }}}
$$
%The converse is similar.

\paragraph{\bf Case $\restr{\cha}{ \nil  } \equiv \nil$ } \quad \\ This case is easily proven by appealing to rule \rulename{t:Weak}.


\paragraph{\bf Cases $P \para Q  \equiv Q \para P$ and $(P \para Q )\para R \equiv P \para (Q \para R)$} \quad \\ 
In both cases, the proof  follows by commutativity and associativity of $\cup$ and $\uplus$ (cf. Def.~\ref{d:interf}).

\paragraph{\bf Case $\restr{\cha}{\restr{\cha'}{P}} \equiv \restr{\cha'}{\restr{\cha}{P}}$} \quad \\  This case is similar to previous ones.
%\end{description}
\end{proof}

The following auxiliary result concerns substitutions for channels, expressions, and process variables.
Observe how the case of process variables has been relaxed so as to allow substitution 
with a process with ``smaller'' interface (in the sense of \intpr). This extra flexibility is in line
with the typing rule for located processes (rule~\rulename{t:Loc}), and will be useful later on in proofs.
%In order to prove the subject reduction theorem we need some auxiliary results. The first lemma handles substitutions.

\begin{lemma}[Substitution Lemma]\label{lem:substitution}
\quad 
\begin{enumerate}
 \item \label{subchavar}If $\judgebis{\env{\Gamma}{ \Theta}}{P}{\type{\ActS,x:\ST}{\INT}}$ then $\judgebis{\env{\Gamma}{ \Theta}}{P\sub{\cha^p}{x}}{\type{\ActS, \cha^p:\ST }{\INT}}$ %\jp{This statement should be different, I think.} \todo{check if this new formulation" is what you were thinking} 
  \item \label{subvalvar}If $\judgebis{\env{\Gamma, \tilde{x}:\tilde{\tau}}{ \Theta}}{P}{\type{\ActS}{\INT}}$ and $\Gamma \vdash \tilde{e}:\tilde{\tau}$ then $\judgebis{\env{\Gamma}{ \Theta}}{P\sub{\tilde{e}}{\tilde{x}}}{\type{\ActS}{\INT}}$. 
 % \item If $\judgebis{\env{\Gamma}{ \Theta}}{P}{\type{\ActS}{\INT}}$  then $\judgebis{\env{\Gamma}{ \Theta}}{P\sub{\cha^p}{x}}{\type{\ActS\sub{\cha^p}{x}}{\INT}}$. 
   \item \label{subprovar} If $\judgebis{\env{\Gamma}{ \Theta,\mathsf{X}:\INT}}{P}{\type{\emptyset}{\INT_1}}$ and $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\emptyset}{\INT'}}$ with $\INT' \sqsubseteq \INT$  then \\ 
   $\judgebis{\env{\Gamma}{\Theta}}{P\sub{Q}{\mathsf{X}}}{\type{\emptyset}{\INT'_1}}$ with $\INT'_1 \sqsubseteq \INT_1$. %\jp{in the proof, it'd be better to explain why this inequality holds}
\end{enumerate}
\end{lemma}
\begin{proof}
Easily shown by induction on the structure of $P$.
\end{proof}
 
As reduction may occur inside contexts, in proofs it is useful to refer to the 
 %Then, we need to introduce how to manipulate contexts, to this aim we define the 
 type of the processes inside a context.

\begin{definition}[Type of contexts]
Let $C$ be a context as in Def.~\ref{d:context}. 
The type of $C$, denoted $\typecontx{C}{ \Gamma}{ \Theta}$, is 
inductively defined as a pair:
$$
\begin{array}{ll}
 \typecontx{\bullet}{ \Gamma}{ \Theta} &= (\emptyset, \emptyset)\\
 \typecontx{\compo{l}{h}{C \para P}}{ \Gamma}{ \Theta}& = (\Pi_1( \typecontx{C}{\Gamma}{ \Theta}) \cup \ActS, ~\Pi_2(\typecontx{C}{\Gamma}{ \Theta}) \addelta \INT) \qquad \qquad \qquad \ \\
  & \hfill \text{ if } ~\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}
\end{array}
$$
where $\Pi_1(\typecontx{C}{ \Gamma}{ \Theta})$ 
(resp. $\Pi_2(\typecontx{C}{ \Gamma}{ \Theta})$)
denote the first (resp. second) element of pair 
$\typecontx{C}{ \Gamma}{ \Theta}$.
\end{definition}

%\todo{Cambiare notazione $\typecontx{C}{ \Gamma}{\Theta}$}
Next we state how to infer the type of a context:

\begin{lemma}\label{lem:context}
 Let  $P$ be a process and $C$ a context as in Def.~\ref{d:context}. Then \\ $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_P}{\INT_P}}$ and $\typecontx{C}{ \Gamma}{ \Theta} = (\ActS_C, \INT_C) $ iff 
$\judgebis{\env{\Gamma}{\Theta}}{C\{P\}}{\type{\ActS_C \cup \ActS_P}{\INT_C \addelta \INT_P}}$
\end{lemma}
\begin{proof}
By induction on the structure of the context $C\{\bullet\}$. The proof for the $(\Rightarrow)$ directions follows by observing that the only rules applied for typing $C\{P\}$ are  \rulename{t:Loc} and \rulename{t:Par} that either do not  change or can  only extend $\ActS_P$ and $\INT_P$. The opposite direction $(\Leftarrow)$, similarly, relies on the typing inversion on the same rules
 \rulename{t:Loc} and \rulename{t:Par}.
\end{proof}


\begin{newnotation}
In the proof of Theorem~\ref{th:subred}, we shall use the following notation 
to denote an use of  Lemma \ref{lem:context}:
$$
\infer={\judgebis{\env{\Gamma}{\Theta}}{C\{P\}}{\type{\ActS_P, \ActS_C}{ \INT_P \uplus \INT_C}}}		  
    {\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_P}{ \INT_P }}}
$$
\end{newnotation}




%\jp{Now I tend to think that we may need something like Lemma \ref{lem:context}. 
%The point is that in the proof we would like to get rid of contexts, justifying the ellipses (not to enclose processes within contexts, as Lemma 9 does). 
%With such a lemma, we could "go up" in the typing tree until we have something without contexts.
%At that point, we apply something (say, a substitution lemma). Then, we conclude by "going down" again, reconstructing the context. The proof would be indeed by structural induction on the context (base case: empty contexts--trivial; cases for locations/restriction are easy by IH and typing inversion).}

%\jp{Why not writing this as a corollary?}
%\todo{Maybe just a remark}
% Notice that previous lemma allows us to conclude that, given a process $P$ and a context $C$, if $\judgement{\Gamma}{\Theta}{C[P]}{\ActS}{\INT}$ then there exists $\Gamma, \Theta, \ActS', \INT'$ such that $\judgement{\Gamma}{\Theta}{P}{\ActS'}{\INT'}$.


%\todo{Subject reduction works for balanced environments; we need to introduce that notion. }

\begin{definition}[Balanced Typings]\label{d:balanced}
We say a typing 
$\ActS$ is balanced iff 
for all $\kappa^p:\ST \in \ActS$ (resp. $[\kappa^p:\ST] \in \ActS$)
then also 
$\kappa^{\overline{p}}: \overline{\ST} \in \ActS$ (resp. $[\kappa^{\overline{p}}: \overline{\ST}] \in \ActS$).
%for all $\kappa^p:\ST \in \ActS$ then also 
%$\kappa^{\overline{p}}: \overline{\ST} \in \ActS$, and 
%for all $[\kappa^p:\ST] \in \ActS$ then also
%$[\kappa^{\overline{p}}: \overline{\ST}] \in \ActS$.
\end{definition}

The final requirement for proving that typing ensures safety is the subject reduction theorem below.

\begin{theorem}[Subject Reduction]\label{th:subred}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced and $P \pired Q$ then 
 $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS'}{\INT'}}$, for some $\INT'$ and balanced $\ActS'$.
\end{theorem}


\begin{proof}
We assume that $\tilde{e} \downarrow \tilde{c}$ is a type preserving operation, for every $\tilde{e}$.
The proof proceeds by induction on the rule applied in the reduction. 
%\begin{description}
\paragraph{\bf Case \rulename{r:Open}}
\begin{multline*} 
E\big\{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}\big\} \pired  \\
E^{++}_{} \big\{\restr{\cha}{\big({C^{+}_{}\{P_1\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }\big)\big\} } 
\end{multline*}
The assumption  $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_{2}\}\big\} }{\type{\ActS}{\INT}}$
is obtained by the following derivation tree using Lemma \ref{lem:context} ($\Leftarrow$) three times,  and  
inversion on rules \rulename{t:Accept}, \rulename{t:Request}, and \rulename{t:Par}:
$$
\infer=
{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_{2}\}\big\}}{\type{\ActS}{\INT}}}
{
	\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_{2}\}}{\type{\ActS'}{\INT'}}}
{    (\ref{eq:typeaccept})
%
&
%
(\ref{eq:typerequest})
}}
$$
where subtrees (\ref{eq:typeaccept}) and (\ref{eq:typerequest}) are as follows:
\begin{equation}\label{eq:typeaccept}
\infer={\judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{a}{x}.P_1\}}{\type{\ActS_1'}{ \INT_1'\addelta \inter{a}{\ST}{1} }}}		  
    { 
 	\infer{\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P_1}{\type{\ActS_1}{ \INT_1\addelta \inter{a}{\ST}{1} }}}
  {\Gamma \vdash a: \langle \ST , \overline{\ST } \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, x:\ST}{\INT_1}} }}
\end{equation}


\begin{equation}\label{eq:typerequest}
\infer={\judgebis{\env{\Gamma}{\Theta}}{D\{\nopenr{a}{y}.P_{2} \}}{ \type{\ActS'_2}{ \INT'_2\addelta \inter{a}{\overline{\ST}}{1} }}}
	{\infer{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{y}.P_{2}}{ \type{\ActS_2}{ \INT_2\addelta \inter{a}{\overline{\ST}}{1} }}}
	{\Gamma \vdash a: \langle \ST , \overline{\ST} \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_{2}}{\type{\ActS_2, y:\overline{\ST }}{\INT_2}}}
}
 \end{equation}


By Lemma \ref{lem:context} ($\Leftarrow$) we have $\ActS_1 \subseteq \ActS_1'$, $\ActS_2 \subseteq \ActS_2'$, and $\ActS' \subseteq \ActS$ where $\ActS' = \ActS'_1 \cup \ActS'_2$. Moreover, we infer $\INT_1 \sqsubseteq \INT_1'$, $\INT_2 \sqsubseteq \INT_2'$, and $\INT' \sqsubseteq \INT$ where $ \INT' = (\INT'_1 \addelta \inter{a}{\ST}{1}) \addelta (\INT'_2\addelta \inter{a}{\overline{\ST}}{1} )$. 
 Now, using Lemma~\ref{lem:substitution}(\ref{subchavar}) on $P_1$ and $P_2$, we have:
 \begin{itemize}
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_1\sub{\cha^+}{x}}{ \type{\ActS_1, \cha^+:\ST}{\INT_1}}$.
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}$.
 \end{itemize}
By using Lemma \ref{lem:context}($\Rightarrow$)  and typing rules \rulename{t:Par} and \rulename{t:CRes} we may then reconstruct the derivation leading to contexts $C, D$, and $E$. Let 
$$R \triangleq {{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }},$$
\begin{equation}\label{eq:typeacceptsub}
\infer={\judgebis{\env{\Gamma}{\Theta}}{C^{+}\{P_{1}\sub{\cha^+}{x}\}}{\type{\ActS_1', \cha^+:\ST}{ \INT_1' }}}		  
    { 
    	\judgebis{\env{\Gamma}{ \Theta}}{P_{1}\sub{\cha^+}{x}}{ \type{\ActS_1, \cha^+:\ST}{\INT_1}}}
\end{equation}
and
\begin{equation}\label{eq:typerequestsub}
 \infer={\judgebis{\env{\Gamma}{\Theta}}{D^{+}\{P_{2}\sub{\cha^-}{y}\}}{\type{\ActS'_2,\cha^- :\overline{\ST } }{\INT'_2}}}
	{\judgebis{\env{\Gamma}{ \Theta}}{P_{2}\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}}
\end{equation}
we thus obtain:
$$
\infer=
{\judgebis{\env{\Gamma}{\Theta}}{E^{++}_{} \big\{\restr{\cha}{R} \big\} }{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT''}}}
{
	\infer{\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{R}}{\type{\ActS', [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT_1' \cup \INT_2'}}}
{\infer{\judgebis{\env{\Gamma}{\Theta}}{{R }}{\type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \cup \INT_2'}}}{
(\ref{eq:typeacceptsub})
%
&
%
	(\ref{eq:typerequestsub})
}
}}
$$
where by Lemma \ref{lem:context}, we have $\INT'' \sqsubseteq \INT_1' \cup \INT_2'$ and 
thus concluding this case. 

\paragraph{\bf Case \rulename{r:ROpen}} 
\begin{multline*}
          E\big\{C\{\repopen{a}{x}.P_1\}  \para  D\{\nopenr{a}{y}.P_2\} \big\}  \pired  \\
E^{++}_{}\big\{\restr{\cha}{\big({C^{+}_{}\{P_1\sub{\cha^+}{x}  \para \repopen{a}{x}.P_1 \}  \para  D^{+}_{}\{P_2\sub{\cha^-}{y}\} }\big)}\big\}  
         \end{multline*}

The assumption $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\repopen{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}\big\} }{\type{\ActS}{\INT}}$ is obtained by the following derivation tree using Lemma \ref{lem:context}($\Leftarrow$) three times and inversion on  rules \rulename{t:RepAccept}, \rulename{t:Request}, and \rulename{t:Par}:
$$
\infer=
{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\repopen{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}\big\}}{\type{\ActS}{\INT}}}
{ \infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\repopen{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}}{\type{\ActS'}{\INT'}}}
{
(\ref{eq:bangaccept})
%
&
%
(\ref{eq:bangrequest})
}}
$$
where (\ref{eq:bangaccept}) and (\ref{eq:bangrequest}) correspond to the subtrees:
\begin{equation}\label{eq:bangaccept}
	\infer={\judgebis{\env{\Gamma}{\Theta}}{C\{\repopen{a}{x}.P_1\}}{\type{\ActS_1'}{ \INT_1'\addelta \inter{a}{\ST}{\infty} }}}		  
    { 
    	\infer{\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P_1}{\type{\emptyset}{\unres( \INT_1)\addelta \inter{a}{\ST}{\infty} }}}
  {\Gamma \vdash a: \langle \ST , \overline{\ST } \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{x:\ST}{\INT_1}} }}
\end{equation}
\begin{equation}\label{eq:bangrequest}
 \infer={\judgebis{\env{\Gamma}{\Theta}}{D\{\nopenr{a}{y}.P_2 \}}{ \type{\ActS'_2}{ \INT'_2\addelta \inter{a}{\overline{\ST}}{1} }}}
	{\infer{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{y}.P_2}{ \type{\ActS_2}{ \INT_2\addelta \inter{a}{\overline{\ST}}{1} }}}
	{\Gamma \vdash a: \langle \ST , \overline{\ST} \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_2}{\type{\ActS_2, y:\overline{\ST }}{\INT_2}}}
}
\end{equation}


where by Lemma~\ref{lem:context} ($\Leftarrow$) we have  $\ActS_2 \subseteq \ActS_2'$,  $\ActS' \subseteq \ActS$, and $\ActS' = \ActS'_1 \cup \ActS'_2$. Moreover, $\INT_1 \sqsubseteq \INT_1'$, $\INT_2 \sqsubseteq \INT_2'$ and $\INT' \sqsubseteq \INT$ where $ \INT' = (\INT'_1 \addelta \inter{a}{\ST}{\infty}) \addelta (\INT'_2\addelta \inter{a}{\overline{\ST}}{1} )$. 
 Now, applying Lemma~\ref{lem:substitution}(\ref{subchavar}) to $P_1$ and $P_2$, we have:
 \begin{itemize} %[$-$]
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_1\sub{\cha^+}{x}}{ \type{ \cha^+:\ST}{\INT_1}}$.
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}$.
 \end{itemize}
We also have that $\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P_1}{\type{\emptyset}{ \INT_1\unres \addelta \inter{a}{\ST}{\infty} }}$.
By applying Lemma~\ref{lem:context} ($\Rightarrow$) and typing rules \rulename{t:Par} and \rulename{t:CRes} we obtain the following derivation trees. Let $R = P_1\sub{\cha^+}{x}  \para \repopen{a}{x}.P_1$
by using rule \rulename{t:Par} and by noticing that $\INT_1\unres \addelta \INT_1 = \INT_1\unres  $ we know that 
$$\judgebis{\env{\Gamma}{\Theta}}{R}{\type{\cha^+:\ST}{ \unres(\INT_1)\addelta \inter{a}{\ST}{\infty} }}$$
Hence by defining:
$$
Q \triangleq C^{+}_{}\{R \}  \para  D^{+}_{}\{P_2\sub{\cha^-}{y}\} ,
$$
\begin{equation}\label{eq:bangacceptsub}
 \infer={\judgebis{\env{\Gamma}{\Theta}}{C^{+}\{R\}}{\type{\ActS_1', \cha^+:\ST}{ \INT_1' \addelta \inter{a}{\ST}{\infty}}}}		  
    { 
    	\judgebis{\env{\Gamma}{ \Theta}}{R}{ \type{\cha^+:\ST}{ \unres(\INT_1)\addelta \inter{a}{\ST}{\infty} }}}
\end{equation}
and
\begin{equation}\label{eq:bangrequestsub}
 	\infer={\judgebis{\env{\Gamma}{\Theta}}{D^{+}\{P_2\sub{\cha^-}{y}\}}{\type{\ActS'_2,\cha^- :\overline{\ST } }{\INT'_2}}}
	{\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}}
\end{equation}
we have:
$$
\infer=
{\judgebis{\env{\Gamma}{\Theta}}{E^{++}_{}\big\{\restr{\cha}{Q}\big\}  }{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT'' \addelta \inter{a}{\ST}{\infty}}}}
{
	\infer{\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{Q}}{\type{\ActS', [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT_1' \addelta \INT'_2 \addelta \inter{a}{\ST}{\infty}}}}
{\infer{\judgebis{\env{\Gamma}{\Theta}}{{Q }}{\type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \addelta \INT'_2 \addelta \inter{a}{\ST}{\infty}}}}{
(\ref{eq:bangacceptsub}) %
&
%
(\ref{eq:bangrequestsub})
}
}}
$$
thus concluding this case. 

\paragraph{\bf Case \rulename{r:Upd}} 
$$E\big\{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{X}\}\big\} 
\pired   
E_{}\big\{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}\big\}$$
The assumption  $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{X}\}\big\}}{ \type{\ActS}{\INT}}$ is obtained by the following derivation tree using Lemma \ref{lem:context} ($\Leftarrow$) and  
inversion on rules \rulename{t:Par}, \rulename{t:Adapt}, and \rulename{t:Loc}:
$$
\infer=
{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{X}\}\big\}}{ \type{\ActS}{\INT}}}
{\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{X}\}}{ \type{\ActS_1 \cup \ActS_2}{\INT_2' \addelta \INT_4'}}}
{
\infer={\judgebis{\env{\Gamma}{\Theta}}{C\{\component{l}{0}{}{P_1}\} }{ \type{\ActS_1}{\INT_2'}}}
{\infer{\judgebis{\env{\Gamma}{\Theta}}{\compo{l}{0}{P_1}}{ \type{\emptyset}{\INT_2}}}
{ \begin{array}{c}
  \Theta \vdash l:\INT_1\\
   \INT_2 \sqsubseteq \INT_1
   \end{array}
  & \judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\emptyset}{\INT_2} }   }}
&
\infer={\judgebis{\env{\Gamma}{\Theta}}{D\{\adapt{l}{P_2}{X}\}}{ \type{\ActS_2}{\INT_4'}}}{
\infer{\judgebis{\env{\Gamma}{\Theta}}{ \adapt{l}{P_2}{X}}{ \type{\emptyset}{\emptyset}}}
{\Theta \vdash l:\INT_1  &  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT_1}}}{P_2}{\type{\emptyset}{ \INT_3 }}}}
}}
$$
By Lemma \ref{lem:context} ($\Leftarrow$) we have $\ActS_1 \cup \ActS_2 \subseteq \ActS$, $\INT_2 \sqsubseteq \INT_2'$, $\INT_4 \sqsubseteq \INT_4'$, and $\INT_2' \addelta \INT_4' \sqsubseteq \INT$. 
By Lemma \ref{lem:substitution}(\ref{subprovar}) we have  $\judgebis{\env{\Gamma}{\Theta}}{ P_2\sub{P_1}{\mathsf{X}}}{\type{\emptyset}{\INT'_3}}$ with $\INT'_3 \sqsubseteq \INT_3$, thus process $E_{}\big\{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}\big\}$ can be typed by means of Lemma~\ref{lem:context} ($\Rightarrow$) and rule \rulename{t:Par}:

$$
\infer={\judgebis{\env{\Gamma}{\Theta}}{E_{}\big\{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}\big\}}{ \type{\ActS}{\INT'}}}{
\infer
{\judgebis{\env{\Gamma}{\Theta}}{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}}{ \type{\ActS_1 \cup \ActS_2}{\INT''_3 \addelta \INT_4'}}}
{\infer={\judgebis{\env{\Gamma}{\Theta}}{ C\{P_2\sub{P_1}{\mathsf{X}}\} }{\type{\ActS_1}{\INT''_3}}}{
\judgebis{\env{\Gamma}{\Theta}}{ P_2\sub{P_1}{\mathsf{X}}}{\type{\emptyset}{\INT'_3}}}
&
\infer={\judgebis{\env{\Gamma}{\Theta}}{D\{\nil\}}{ \type{\ActS_2}{\INT_4'}}}{
\judgebis{\env{\Gamma}{\Theta}}{\nil}{ \type{\emptyset}{\emptyset}}}
}}
$$
where by Lemma \ref{lem:context}($\Rightarrow$) we know $\INT_3'' \sqsubseteq \INT'_3$ and $\INT_3'' \addelta \INT_4' \sqsubseteq \INT'$.
This concludes the analysis for this case.

\paragraph{\bf Case \rulename{r:I/O}} 
$$E\big\{C\{\outC{\cha^{\,p}}{\tilde{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\tilde{x}}.P_2\}\big\} 
\pired 
E\big\{C\{P_1\} \para  D\{P_2\sub{\tilde{c}\,}{\tilde{x}}\}\big\} \quad (\tilde{e} \downarrow \tilde{c})$$
The assumption is $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\outC{\cha^{\,p}}{\tilde{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\tilde{x}}.P_2\}\big\} }{ \type{\ActS}{\INT}}$ with $\ActS$ balanced and we thus obtain the following derivation that employs Lemma~\ref{lem:context} ($\Leftarrow$) three times and inversion on rules  \rulename{t:Par}, \rulename{t:In}, and \rulename{t:Out}, we let
$$
R \triangleq C\{\outC{\cha^{\,p}}{\tilde{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\tilde{x}}.P_2\}
$$
$$
\infer={\judgebis{\env{\Gamma}{\Theta}}{E\big\{R\big\} }{ \type{\ActS}{\INT}}}
{\infer
{
\judgebis{\env{\Gamma}{\Theta}}{R} {\type{\ActS_1' \cup \ActS_2', \cha^p:!(\tilde{\capab}).{\ST}, \cha^{\overline{p}}:?(\tilde{\capab}).\overline{\ST} }{ \INT_1' \addelta \INT_2'}}}
{ (\ref{eq:out})
&
(\ref{eq:in})
}}
$$
where subtrees (\ref{eq:out}) and (\ref{eq:in}) are as follows:
\begin{equation}\label{eq:out} 
\infer={\judgebis{\env{\Gamma}{\Theta}}{C\{\outC{\cha^{p}}{\tilde{e}}.P_1\} } {\type{\ActS_1',  \cha^p:!(\tilde{\capab}).{\ST} }{ \INT_1' }}}{
  \infer
{\judgebis{\env{\Gamma}{\Theta}}{\outC{\cha^p}{\tilde{e}}.P_1}{\type{\ActS_1, \cha^p:!(\tilde{\capab}).{\ST}}{ \INT_1}}}
{\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, \cha^p:{\ST}}{ \INT_1}} & \Gamma \vdash \tilde{e}:\tilde{\capab}}}
\end{equation}
\begin{equation}\label{eq:in}
 \infer={\judgebis{\env{\Gamma}{\Theta}}{ D\{\inC{\cha^{\overline{p}}}{\tilde{x}}.P_2\}}{\type{ \ActS_2', \cha^{\overline{p}}:?(\tilde{\capab}).\overline{\ST}}{ \INT_2'}}}
{
  \infer
{\judgebis{\env{\Gamma}{\Theta}}{\inC{\cha^{\overline{p}}}{\tilde{x}}.P_1 }{\type{\ActS_2, \cha^{\overline{p}}:?(\tilde{\capab}).\overline{\ST}}{ \INT_2}}}
{\judgebis{\env{\Gamma, \tilde{x}:\tilde{\capab}}{\Theta}}{P_2}{\type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{\INT_2}}}}
\end{equation}
where Lemma~\ref{lem:context} ($\Leftarrow$) ensures $\ActS_1 \subseteq \ActS_1'$, $\ActS_2 \subseteq \ActS_2'$, $\ActS \subseteq \ActS_1' \cup \ActS_2', \cha^p:!(\tilde{\capab}).{\ST}, \cha^{\overline{p}}:?(\tilde{\capab}).\overline{\ST} $, $\INT_1 \sqsubseteq \INT_1'$, $\INT_2 \sqsubseteq \INT_2'$, and $ \INT \sqsubseteq \INT_1 \uplus \INT_2$.

Now, by Lemma \ref{lem:substitution}(2)  we know $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\tilde{c}}{\tilde{x}}}{\type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{\INT_2}}$ with $\tilde{e} \downarrow \tilde{c}$. Moreover by Lemma \ref{lem:context} ($\Rightarrow$) and rule \rulename{t:Par}  we obtain the following type derivation:
 $$
\infer={\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{P_1\} \para  D\{P_2\sub{\tilde{c}\,}{\tilde{x}}\}\big\} }{ \type{\ActS'}{\INT}}}
{\infer
{
\judgebis{\env{\Gamma}{\Theta}}{C\{P_1\} \para  D\{P_2\sub{\tilde{c}\,}{\tilde{x}}\}} {\type{\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}:\overline{\ST} }{ \INT_1' \addelta \INT_2'}}}
{\infer={\judgebis{\env{\Gamma}{ \Theta}}{C\{P_1\}}{\type{\ActS_1', \cha^p:\ST}{\INT_1'}}}
{
\judgebis{\env{\Gamma}{ \Theta}}{P_1}{\type{\ActS_1, \cha^p:\ST}{\INT_1}}}
   &
\infer={\judgebis{\env{\Gamma}{\Theta}}{D\{P_2\sub{\tilde{c}\,}{\tilde{x}}\}}{\type{\ActS_2', \cha^{\overline{p}}:\overline{\ST}}{ \INT_2'}}}{
\judgebis{\env{\Gamma}{\Theta}}{P_2\sub{\tilde{c}\,}{\tilde{x}}}{\type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{ \INT_2}} }}}
$$ 
Since by inductive hypothesis  $\ActS_1'$ and $\ActS_2'$ are balanced, we infer that  $\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}:\overline{\ST}$ is balanced as well; this concludes the proof for this case.

%%%%%%%%%%%%%%%%% 
\paragraph{\bf Case \rulename{r:Pass}} $$E\big\{C\{\throw{\cha^{\,p}}{\cha_1^{\,q}}.P_1\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.P_2\}\big\}\pired E\big\{C^{-}\{P_1\} \para  D^{+}\{P_2\sub{\cha_1^{\,q}}{x}\}\big\}$$

By assumption we have  $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\throw{\cha^{\,p}}{\cha_1^{\,q}}.P_1\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.P_2\}\big\}}{ \type{\ActS}{\INT}}$ with $\ActS$ balanced. Using   Lemma \ref{lem:context} ($\Leftarrow$) and inversion on rules \rulename{t:Par}, \rulename{t:Cat}, and \rulename{t:Thr} we infer:
$$
\infer=
	{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\throw{\cha^{\,p}}{\cha_1^{\,q}}.P_1\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.P_2\}\big\}}{ \type{\ActS}{\INT}}}
{\infer
	{\judgebis{\env{\Gamma}{\Theta}}{C\{\throw{\cha^{p}}{\cha_1^{\overline{p}}}.P_1\} \para  D\{\catch{\cha^{\overline{p}}}{x}.P_2\}}{ \type{\ActS'}{\INT'}}}
	{
	(\ref{eq:throw})
	&
	(\ref{eq:catch})
	}}
$$
where (\ref{eq:throw}) and (\ref{eq:catch}) correspond to the subtrees:
\begin{equation}\label{eq:throw}
 \infer=
		{\judgebis{\env{\Gamma}{\Theta}}{C\{\throw{\cha^{p}}{\cha_1^{q}}.P_1\} }{ \type{\ActS'_1, \cha^p:!(\ST).\overline{\STT}, \cha_1^{q}:\ST}{ \INT'_1}}}
		{\infer
{\judgebis{\env{\Gamma}{\Theta}}{\throw{\cha^p}{\cha_1^{q}}.P_1}{\type{\ActS_1, \cha^p:!(\ST).\overline{\STT}, \cha_1^{q}:\ST}{ \INT_1}}}
{\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, \cha^p:\overline{\STT}}{ \INT_1}} 
		}}
\end{equation}
\begin{equation}\label{eq:catch}
 \infer=
		{\judgebis{\env{\Gamma}{\Theta}}{ D\{\catch{\cha^{\overline{p}}}{x}.P_2\}}{ \type{\ActS'_2, \cha^{\overline{p}}:?(\ST).\STT}{ \INT'_2}}}
		{\infer
{\judgebis{\env{\Gamma}{\Theta}}{\catch{\cha^{\overline{p}}}{x}.P_2 }{\type{\ActS_2, \cha^{\overline{p}}:?(\ST).\STT}{ \INT_2}}}
{\judgebis{\env{\Gamma}{\Theta}}{P_2}{\type{\ActS_2, \cha^{\overline{p}}:\STT, x:\ST}{\INT_2}}}	
}
\end{equation}
and where by Lemma \ref{lem:context} ($\Leftarrow$) ensures $\ActS_1 \subseteq \ActS_1'$, $\ActS_2 \subseteq \ActS_2'$, $\ActS' \subseteq \ActS$ and $\ActS' = \ActS'_1 \cup \ActS'_2,  \cha^p:!(\ST).\overline{\STT}, \cha_1^q:\ST, \cha^{\overline{p}}:?(\ST).\STT$. Moreover we have $\INT_1 \sqsubseteq \INT_1'$, $\INT_2 \sqsubseteq \INT_2'$, $\INT' \sqsubseteq \INT$ and $\INT' = \INT'_1 \addelta \INT'_2$. Notice that as $\ActS$ is balanced, in $\ActS$ there is a $\cha_1^{\overline{q}}:\overline{\ST}$.

Then by Lemma \ref{lem:substitution}(\ref{subchavar}) we have $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha_1^q}{x}}{\type{\ActS'_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT'_2}}$ thus obtaining the following typing tree where we have used Lemma \ref{lem:context} ($\Rightarrow$) and rule \rulename{t:Par}, we also use the following subtree:
\begin{equation}\label{eq:pass}
 \infer=
		{\judgebis{\env{\Gamma}{\Theta}}{ D^{+}\{P_2\sub{\cha_1^{q}}{x}\}}{ \type{\ActS'_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT'_2}}}
		{\judgebis{\env{\Gamma}{\Theta}}{P_2\sub{\cha_1^{q}}{x}}{\type{\ActS_2, \cha^+:\STT, \cha_1^q:\ST}{\INT_2}}	
}
\end{equation}
$$
\infer=
	{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C^{-}\{P_1\} \para  D^{+}\{P_2\sub{\cha_1^{q}}{x}\}\big\}}{ \type{\ActS''}{\INT}}}
{\infer
	{\judgebis{\env{\Gamma}{\Theta}}{C^{-}\{P_1\} \para  D^{+}\{P_2\sub{\cha_1^{q}}{x}\}}{ \type{\ActS'_1 \cup \ActS'_2, \cha^p:\overline{\STT}, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{\INT'}}}
	{\infer=
		{\judgebis{\env{\Gamma}{\Theta}}{C^{-}\{P_1\} }{ \type{\ActS'_1, \cha^p:\overline{\STT}}{ \INT'_1}}}
		{\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, \cha^p:\overline{\STT}}{ \INT_1}} 
		}
	& (\ref{eq:pass})
	}}
$$
Notice that by construction $\ActS''$ is balanced. It is also important to see how the contexts $C^{-}$ and $D^{+}$ correctly implement the fact that the number of active sessions is changed after delegating session $\kappa_1$ to process $P_2$.
 This concludes the proof for this case.


% 
\paragraph{\bf Cases \rulename{r:IfTr} and \rulename{r:IfFa}} Follows by an ease induction on the derivation tree.

% 
\paragraph{\bf Case \rulename{r:Close}} This case follows the same reasoning as in  \rulename{r:Open} case.
% 
\paragraph{\bf Case \rulename{r:Branch}} This case is similar to  previous \rulename{r:I/O} case. 
% 
\paragraph{\bf Case \rulename{r:Str}} Follows from Theorem~\ref{th:congr} (Subject Congruence).
% 
\paragraph{\bf Case \rulename{r:Par}} Follows by induction and by applying rule $\rulename{t:Par}$.
%
\paragraph{\bf Case \rulename{r:Res}} Follows by induction and by the fact that  $\ActS$ is balanced. Indeed, by hypothesis and by inversion on rule \rulename{t:CRes} all the occurences of bracketed assignements ($[\cha^p:\ST]$) are necessarily balanced thus making it possible to apply the inductive hypothesis to the premise of the rule and concluding the analysis of this case and the proof of the theorem.
% \end{description}
\end{proof}

We are now ready to state our first main result:
 the \emph{absence of communication errors} for well-typed processes.
Recall that our notion of error process has been given in 
Definition~\ref{d:kred}.


\begin{theorem}[Typing Ensures Safety]\label{t:safety}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced
then $P$ never reduces into an error.
\end{theorem}

\begin{proof}
We assume, towards a contradiction, that there exists a $P_1$ 
such that ~$P \pired^* P_1$ and $P_1$ is an error process.
By Theorem~\ref{th:subred} (Subject Reduction), $P_1$ is well-typed under a balanced typing $\D_1$.
Following Def.~\ref{d:kred}, there are two possibilities for $P_1$, namely 
it contains %(i)  exactly one $\kappa$-process, 
(i) exactly two $\kappa$-processes which do not form a $\kappa$-redex and (ii) three or more $\kappa$-processes.
Consider the second possibility.   
There are several combinations;
by inversion on rule \rulename{t:CRes}
we have that,
for some session types $\alpha_1$ and $\alpha_2$,
% either $\{\kappa^{p}: \alpha_1, \kappa^{\overline{p}}: \alpha_2\} \subseteq \D_1$ or  
$\{[\kappa^{p}: \alpha_1], [\kappa^{\overline{p}}: \alpha_2]\} \subseteq  \D_1$. 
In all cases, since the two $\kappa$-processes do not form a $\kappa$-redex then, necessarily, 
 $\alpha_1 \neq \overline{\alpha_2}$. This, however, contradicts the definition of balanced typings (Def.~\ref{d:balanced}).
The second possibility again contradicts Def.~\ref{d:balanced}, 
as in that case $\D_1$ would capture the fact that
at least one $\kappa$-process does not have a complementary partner for forming a $\kappa$-redex.
We thus conclude that well-typed processes never reduce to an error.
\end{proof}


\subsection{Session Consistency}\label{ss:consist}

We now investigate \emph{session consistency}: this is to 
%address a basic consequence of considering
enforce a basic discipline on 
the interplay of communicating behavior (i.e., session interactions) 
and evolvability behavior (i.e., update actions). 
Informally, %we say that a %session on channel $\kappa$ 
a process $P$
is called \emph{consistent} 
if %it is never disrupted by an evolvability step. 
%That is, 
whenever  %session on $\kappa$ is active and 
it has 
a $\kappa$-redex (cf. Def.~\ref{d:kred}) then 
possible interleaved update actions do not destroy such a redex.
%performing an update action does not affect the behavior of active sessions.

Below, we formalize this intuition. 
Let us write $P \pired_{\text{upd}} P'$ 
for any reduction inferred using rule $\rulename{r:Upd}$, possibly followed
by uses of rules $\rulename{r:Res}$, $\rulename{r:Str}$, and $\rulename{r:Par}$.
We then define:

%\begin{definition}[Session Consistency]\label{d:consist}
%Let $P$ be a process. 
%A session on channel $\kappa$ is \emph{consistent} in $P$ if,
%for all process $P', P''$ and contexts $E, C, D$ 
%such that 
%$$P \pired^{*} P' \equiv (\nu \tilde{\kappa})E\big\{C\{P_1\} \para  D\{P_2\}\big\}$$
%where $P_1$ and $P_2$ make $P'$ a $\kappa$-redex
%and $P' \pired_{\text{upd}} P''$, then there exist contexts $E', C'$, and $D'$ such that
%$$P'' \equiv (\nu \tilde{\kappa})E'\big\{C'\{P_1\} \para  D'\{P_2\}\big\}$$
%\end{definition}
%
%Hence, consistency on a session $\kappa$ %as formalized by Def.~\ref{d:consist} 
%says that update actions do not destroy $\kappa$-redexes. 
%Clearly, this definition does not rule out the possibility of interleaving intra-session communication 
%and update steps: it just requires update actions to reconfigure parts of the system not currently engaged into active sessions. 
%We find that giving priority to disciplined structured behavior over 
%runtime adaptation steps, as intended by this notion of consistency, 
%is a rather natural requirement.
%
%\jp{I feel consistency should be a property of processes, and focused on what the updates preserve
%rather than on what the sessions do. Hence I suggest stating consistency as:}

\begin{definition}[Consistency]\label{d:consis}
A process $P$ is \emph{update-consistent} 
if and only if,
 for all $P'$ and $\kappa$ 
such that $P \pired^{*} P'$ and $P'$ contains a $\kappa$-redex, 
if $P' \pired_{\text{upd}} P''$
then $P''$ contains a $\kappa$-redex.
\end{definition}

Recall that a \emph{located} $\kappa$-redex is a $\kappa$-redex in which one or both of
its constituting $\kappa$-processes are contained by least one located process.
This way, for instance, 
$$
\begin{array}{c}
\scomponent{l_2}{\,\scomponent{l_1}{\inC{\kappa^{\,p}}{\tilde{x}}.P_1}  \para \outC{\kappa^{\,\overline{p}}}{v}.P_2\,} \\
\scomponent{l_1}{\inC{\kappa^{\,p}}{\tilde{x}}.P_1}  \para \scomponent{l_2}{\outC{\kappa^{\,\overline{p}}}{v}.P_2} \\
\scomponentbig{l_1}{\inC{\kappa^{\,p}}{\tilde{x}}.P_1  \para \outC{\kappa^{\,\overline{p}}}{v}.P_2} 
\end{array}
$$
are located $\kappa$-redexes, whereas $\inC{\kappa^{\,p}}{\tilde{x}}.P_1  \para \outC{\kappa^{\,\overline{p}}}{v}.P_2$ is not.
From the point of view of consistency, the distinction between located and unlocated $\kappa$-redexes is relevant:
since update actions result from synchronizations on located processes, 
unlocated $\kappa$-redexes are always preserved by update actions, 
whereas located $\kappa$-redexes may be destroyed by a  update action.
We have the following auxiliary proposition.

\begin{proposition}\label{p:nonzero}
Let 
$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$, with $\ActS$ balanced, 
be a well-typed process containing  
a $\kappa$-redex, for some $\kappa$. We have:
\begin{enumerate}[(a)]
\item $\ActS = \ActS', \kappa^p: \ST,  \kappa^{\overline{p}}:\overline{\ST}$
~~or~~ $\ActS = \ActS', [\kappa^p: \ST],  [\kappa^{\overline{p}}:\overline{\ST}]$
, for some session type $\ST$, and a balanced $\ActS'$.
\item If the $\kappa$-redex is located, then the runtime annotation for the location(s) hosting its 
constituting $\kappa$-processes is different from zero.
\end{enumerate}

\begin{proof}
Part~(a) is immediate from our definition of typing judgment, in particular from the fact that typing $\D$
records the types of currently active sessions, as implemented by channels such as $\kappa$.
Part~(b) follows directly by definition of typing rule \rulename{t:Loc} and part (a), observing that typing relies on the cardinality of $\D$
to compute (non zero) runtime annotations for locations. 
% and the fact that $\kappa$-redexes are essentially dual active sessions recorded in $\D$.
\end{proof}

\end{proposition}

\begin{theorem}[Typing Ensures Update Consistency]\label{t:consist}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$, with $\ActS$ balanced,
then $P$ is update consistent.
\end{theorem}

\begin{proof}
%By contradiction.
We assume, towards a contradiction, that there exist $P_1$, $P_2$, and $\kappa_1$ such that
(i)~$P~\pired^*~P_1$, (ii)~$P_1$ has a $\kappa_1$-redex,  (iii)~$P_1 \pired_{\text{upd}} P_2$, and 
(iv)~$P_2$ does not have a $\kappa_1$-redex.  Without loss of generality, 
we suppose that the reduction $P_1 \pired_{\text{upd}} P_2$ is due to a synchronization on location $l_1 \in \T$.
Since the $\kappa_1$-redex is destroyed by the update action from $P_1$ to $P_2$, the $\kappa_1$-redex in $P_1$ must necessarily be 
 a located $\kappa_1$-redex, i.e.,  in $P_1$, one or both $\kappa_1$-processes are contained inside $l_1$.
 Now, our reduction semantics (rule \rulename{r:Upd}) decrees that for such an update action to be enabled,
 the runtime annotation for $l_1$ in $P_1$ should be zero. However, by Theorem~\ref{th:subred} (Subject Reduction), we know that $P_1$ is well-typed under a balanced
 typing $\ActS_1$. Then, using well-typedness and Prop.~\ref{p:nonzero}(b)
we infer that the annotation for $l_1$ in $P_1$ must be different from zero: contradiction. 
Hence, update steps which destroy a  
$\kappa$-redex (located and unlocated) can never be enabled from a well-typed process 
  with a balanced typing (such as $P$) nor from any of its derivatives (such as $P_1$). We thus conclude that
  well-typedness implies update consistency.
\end{proof}


% 
 \section{Example: An Adaptable Client/Service Scenario}\label{sec:exam}
To illustrate how
located and update processes
in our framework extend the expressiveness of session-typed languages, we  
recall the  client/server scenario discussed in the Introduction:
% of distributed, interacting services (a client $C_1$ and a replicated service $S$), 
%conveniently represented as located processes:
\begin{eqnarray*}
\mathsf{Sys} & \triangleq &  %\scomponent{l_{0}}{C_1} \para 
%\scomponent{l_{1}}{C_1} \para\bigscomponent{l_2}{\scomponent{r}{S} \para R \, } \quad\text{where:} \vspace{3mm} \\ 
%C_1  &  \triangleq  & \nopenr{a}{c:\overline{\ST}}.\outC{c}{u_1,p_1}.\select{c}{n_1.P_1}.\close{c} \\
%S  &  \triangleq  & \repopen{a}{s:\ST}.\inC{s}{u,p}.\branch{s}{n_1{:}Q_1 \parallel n_2{:}Q_2}.\close{s} 
\scomponent{l_{1}}{C_1} \para\bigscomponent{l_2}{\scomponent{r}{S} \para R \, } \quad\text{where:} \vspace{3mm} \\ 
C_1  &  \triangleq  & \nopenr{a}{x}.\outC{x}{u_1,p_1}.\select{x}{n_1.P_1}.\close{x} \\
S  &  \triangleq  & \repopen{a}{y}.\inC{y}{u,p}.\branch{y}{n_1{:}Q_1 \parallel n_2{:}Q_2}.\close{y} 
\end{eqnarray*}
%Intuitively, 
%$\mathsf{Sys}$ 
%consists of a server $S$ and a client $C_1$.
%They 
%may interact by establishing a session %of type $\sigma$ 
%%between $S$ and $C_1$ %($i \in \{0, 1\}$) 
%using name $a$:
%first, the client sends its user credentials to the server; then, the client chooses one of the two
%services offered by the server. 
%Above, the actual client and server behaviors are  abstracted by processes $P_1$ and $Q_1$, respectively,
%%(resp. $P_1$ and $Q_1$), 
%which are left unspecified.
%Finally, server and client synchronize to close the session.

Recall that process $R$ above represents the platform in which service $S$ is deployed.
We now discuss two
different definitions for $R$:
this is useful to illustrate  the different facets that runtime reconfiguration may adopt in our typed framework.

In what follows, we assume that $Q_i$ realizes a  behavior denoted by type $\beta_i$ ($i \in \{1,2\}$),
and write $\alpha$ to stand for the session type $?(\tau_1,\tau_2).\&\{n_1: \beta_1, n_2: \beta_2\}$ for the server $S$.
Dually, the type for $C_1$ is $\overline{\alpha} = !(\tau_1,\tau_2).\oplus\{n_1: \overline{\beta_1}, n_2: \overline{\beta_2}\}$;
we assume that $P_1$ realizes the session type  $\overline{\beta_1}$.
  
  
%\todo{change $c, s$ with $x$ and say what's $\alpha$.}

\subsection{A Basic Service Reconfiguration: Relocation and Upgrade}
%Here we develop an $R$ which keeps the distributed structure, but adds another service to the menu.
We first suppose that $R$ stands for a simple adaptation routine for $S$ which 
(i)~relocates the service from $r$ to $l_4$, and 
(ii)~sets up a new adaptation routine at $l_4$ which upgrades $S$ with adaptation mechanisms for $Q_1$ and $Q_2$ (denoted $R_{11}$ and $R_{12}$, respectively, and left unspecified):
\begin{eqnarray*}
R & \triangleq &  \adaptn{r}{ \scomponent{l_4}{\mathsf{X}}   \para \adaptn{l_4}{\scomponent{l_4}{S_{\text{new}}}} \, }~ \qquad\text{where:} \\
S_\text{new}  &  \triangleq  & \repopen{a}{y}.\inC{y}{u,p}.\branch{y}{n_1{:}Q^*_1 \parallel n_2{:}Q^*_2\,}.\close{y}  \\
Q^*_1 & \triangleq &  \scomponent{l_5}{Q_1} \para \adaptn{l_5}{R_{11}} \\
Q^*_2 & \triangleq &  \scomponent{l_6}{Q_2} \para \adaptn{l_6}{R_{12}}
\end{eqnarray*}
It is easy to see that the only difference between $S$ and $S_\text{new}$ is in the behavior given at label $n_2$---for 
simplicity, we assume that $Q_2$ and $Q^*_2$ are implementations of the same typed behavior.
For this $R$, using our type system, we can infer that 
$$
\judgebis{\env{\Gamma}{\Theta}}{\mathsf{Sys}}{\type{\emptyset}{\INT_1}} \qquad \text{where:}
$$

\begin{itemize}
\item $\{ a: \langle \ST_\quau, \overline{\ST_\qual} \rangle \} \subseteq \Gamma$
\item $\{ l_1\mapsto a:\overline{\ST_\qual},~ 
l_4\mapsto a:\ST_\quau, ~ r\mapsto a: \ST_\quau , ~ \mathsf{X} \mapsto a: \ST_\quau  \} \subseteq \Theta$
\item $ \INT_1 = \{ \langle a:\overline{\ST}, 1 \rangle ~ \langle a:\ST, \infty \rangle \} $
\end{itemize}
and we have slightly simplified notation for $\Theta$, for readability reasons.

By virtue of Theorem~\ref{t:safety}
typing ensures communications between $C_1$ and $S$ which follow the prescribed session types. Moreover, 
by relying on Theorem~\ref{t:consist}, we know that well-typedness implies consistency, i.e., % between $C$ and $S$, i.e., 
an update action on  $r$ will not be enabled if $C_1$ and $S$ have already initiated a session.
For the scenario above, 
our typed framework ensures that  updates may only take place before a session related to the service on $a$ is established.
Suppose such an action occurs as the first action of $\mathsf{Sys}$ (i.e. service $S$ is immediately relocated, from $r$ to $l_4$): 
$$
\mathsf{Sys} \pired 
%\component{l_{0}}{0}{}{C_0} \para
\component{l_{1}}{0}{}{C_1} \para 
\bigcomponent{l_2}{0}{}{\component{l_4}{0}{}{S}  \para \adaptn{l_4}{\scomponent{l_4}{S_\text{new}}} \,} 
%\pired \component{l_{0}}{0}{}{C_0} \para \component{l_{1}}{0}{}{C_1} \para \bigcomponent{l_2}{0}{}{\component{l_4}{0}{}{S_\text{new}}  \,}  
= \mathsf{Sys}_1
$$
The above reduction represents one of the simplest forms of reconfiguration, one in which the behavior of the located process
is not explicitly changed. 
Still, we observe that runtime relocation may allow to \emph{indirectly} influence the future behavior of a process.
For instance, after relocation the process may 
synchronize with reconfiguration routines (i.e., update processes) not defined for the previous location.
This is exactly what occurs with the above definition for $R$ when relocating $S$ to $l_4$---see below.\footnote{
Conversely, 
update actions that 
remove the enclosing location(s) for a process, or 
relocate it to a location on which there are no update processes available are two ways of preventing future updates.}
Also, the new location may be associated to a larger interface (wrt $\sqsubseteq$) and this could be useful to eventually
enable reconfiguration steps not possible for the process in the old location.

Starting from $\mathsf{Sys}_1$, the service $S$ can be then upgraded to $S_\text{new}$ by synchronizing on $l_4$. We may have:
$$
\mathsf{Sys}_1 
%\pired \component{l_{0}}{0}{}{C_0} \para \component{l_{1}}{0}{}{C_1} \para \bigcomponent{l_2}{0}{}{\component{r_1}{0}{}{S_\text{new}}  \para \adaptn{r}{\scomponent{l_4}{\mathsf{X}}} \,} 
\pired %\component{l_{0}}{0}{}{C_0} \para 
\component{l_{1}}{0}{}{C_1} \para \bigcomponent{l_2}{0}{}{\component{l_4}{0}{}{S_\text{new}}  \,}  = \mathsf{Sys}_2
$$
and by Theorem~\ref{th:subred} we infer that 
$$
\judgebis{\env{\Gamma}{\Theta}}{\mathsf{Sys}_2}{\type{\emptyset}{\INT_1}}
$$

\subsection{Upgrading Behavior and Distributed Structure}\label{ss:behdist}
Suppose now that $R$ stands for the following adaptation routine for $S$:
$$
\begin{array}{ll}
R & \triangleq   \adaptn{r}{\scomponent{r_1}{S_\text{wra}}  \para \scomponent{r_2}{S_\text{rem}} }~ \qquad\text{where:} \\
%S_\text{wra}  &  \triangleq  & \repopen{a}{s:\ST}.\nopenr{b}{d:!(\ST)}.\throw{d}{s}.\close{d} \\
%S_\text{rem} &  \triangleq  &  \repopen{b}{e:?(\ST)}.\catch{e}{s}.\inC{s}{u,p}.\branch{s}{n_1{:}Q_1 \parallel n_2{:}Q_2}.\close{s}.\close{e} 
S_\text{wra} \! \! \! \!&  \triangleq   \repopen{a}{x}.\nopenr{b}{y}.\throw{y}{x}.\close{y} \\
S_\text{rem} \! \! \! \!&  \triangleq    \repopen{b}{z}.\catch{z}{x}.\inC{x}{u,p}.\branch{x}{n_1:Q_1 \parallel n_2:Q_2}.\close{x}.\close{z} 
\end{array}
$$
Above, $S_\text{wra}$ represents a service wrapper which, deployed at $r_1$, acts as a mediator: 
it redirects all client requests on name $a$ 
to the remote service $S_\text{rem}$, defined on name $b$ and deployed at $r_2$. 
Although simple, this service structure is quite appealing: 
by exploiting session delegation, 
it hides 
from clients certain implementation details (e.g.,  name $b$ and location $r_2$), 
therefore simplifying  future reconfiguration tasks---in fact, clients do not need to know about $b$ to execute, and so $S_\text{wra}$ can be transparently upgraded.
The intent with this definition for $R$ is to show an update process that may reconfigure both
the behavior and distributed structure of $S$:
in a single step, 
the monolithic service $S$ is replaced by a more flexible distributed
implementation based on  $S_\text{wra}$ and $S_\text{rem}$ and deployed at $r_1$ and $r_2$ (rather than at $r$).
As we discuss below, $R$ above does not involve process variables, and so the current behavior at $r$ is discarded.
Using our type system, we may infer that 
$$
\judgebis{\env{\Gamma}{\Theta}}{\mathsf{Sys}}{\type{\emptyset}{\INT_1}} \qquad \text{where:}
$$

\begin{itemize}
\item $\{ a: \langle \ST_\quau, \overline{\ST_\qual} \rangle,~  
b: \langle !(\ST)_\qual, ?(\ST)_\quau \rangle \} \subseteq \Gamma$
\item $\{ l_1\mapsto a:\overline{\ST_\qual},~ 
l_2\mapsto a:\ST_\quau \cup b: !(\ST)_\quau \cup b: ?(\ST)_\quau, ~
r\mapsto a: \ST_\quau, ~ 
r_1\mapsto \ST_\quau \cup b: !(\ST)_\quau,~ \\
r_2\mapsto b: ?(\ST)_\quau
\} \subseteq \Theta$
\item $ \INT_1 = \{ \langle a:\overline{\ST}, 1 \rangle ~ \langle a:\ST, \infty \rangle \} $
\end{itemize}
and we have slightly simplified notation for $\Theta$, for readability reasons.

As before,  our typed framework ensures that 
consistent updates may only take place before a session related to the service on $a$ is established.
Suppose such an action occurs as the first action of $\mathsf{Sys}$ (i.e. the definition of service $S$ is immediately updated): %before a session on $a$ is established. 
$$
\mathsf{Sys} \pired 
%\component{l_{0}}{0}{}{C_0} \para
\component{l_{1}}{0}{}{C_1} \para \bigcomponent{l_2}{0}{}{\component{r_1}{0}{}{S_\text{wra}}  \para \component{r_2}{0}{}{S_\text{rem}}} = \mathsf{Sys}'
$$
Because $R$ declares no process variables, this step
formalizes an update operation which \emph{discards} the behavior located at $r$ (i.e., $a: \alpha_\quau$).
To understand why this reconfiguration step is safe, it is crucial to observe that:
\begin{enumerate}[(i)] 
\item  the new service implementation, based on $S_\text{wra}$ and $S_\text{rem}$, respects the prescribed interfaces of the involved locations (i.e., $r_1$ and $r_2$, not used in $\mathsf{Sys}$); 
\item  the interface of location $l_2$ (which hosts the server implementation) can indeed contain the two services on name $b$ implemented by $S_\text{wra}$ and $S_\text{rem}$.
\end{enumerate}
These two important conditions are statically checked by our typing system.
After the reduction it is easy to see that 
$$
\judgebis{\env{\Gamma}{\Theta}}{\mathsf{Sys}'}{\type{\emptyset}{\INT_2}} 
$$
where $\Gamma, \Theta$ are as above and $\INT_2 = \{ a:\overline{\ST_\qual},~ a:\ST_\quau,~b: ?(\ST)_\quau, ~ b: !(\ST)_\quau\}$.
We have $\INT_1 \sqsubseteq \INT_2$: indeed the interface grows, for the updated service  now relies on two service definitions (on names $a, b$) rather than on a single  definition.


% 
 \section{Discussion: Towards More Flexible Interfaces}\label{sec:int}
As argued along the paper, a main contribution of this work is the extension of session types disciplines with a simple notion of \emph{interface}.
Using interfaces, we are able to give
simple and intuitive typing rules for located and update processes---see rules \rulename{t:Loc} and \rulename{t:Adapt} in Table~\ref{tab:ts}.
It is thus legitimate to investigate how to enhance the notion of interface and its associated definitions.
Here we discuss a few alternatives.  
The discussion is kept brief and informal: our aim is to illustrate how the presented framework already provides
a basis for more sophisticated analyses---a formal treatment of these ideas is out of the scope of this paper and is left for future work.

A straightforward enhancement concerns 
the typing of adaptable processes. Consider 
the following alternative  formulation for typing rule \rulename{t:Adapt}:
$$
\cfrac{\Theta \vdash l:\INT_1  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT_1}}}{P}{\type{\emptyset}{ \INT_2 }}  \qquad \boxed{~\INT_1 \intpr \INT_2~}}{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{X}}{\type{\emptyset}{ \emptyset}}} \quad \rulename{t:MonAdapt}  \vspace{2mm}
$$
Clearly, the above rule  is more restrictive than \rulename{t:Adapt}, i.e., it accepts less update processes as typable. 
Still, this rule captures a requirement that may be desirable in several contexts, namely that 
the behavior after adaptation is ``at least'' the behavior offered before, possibly adding new behaviors.
Indeed, by disallowing adaptation routines that discard behavior, rule \rulename{t:MonAdapt} is suitable 
to reason about settings in which adaptation/upgrade actions need to be tightly controlled. 





% and the typing rule 

\begin{table}[!t]
%{\small
\begin{eqnarray*}
&
\inferrule[\rulename{s:End}]{ }{\epsilon \subt \epsilon} 
\qquad
\inferrule[\rulename{s:InE} ]{\forall i.(\tau_i ~ \subt ~\sigma_i)  \qquad \alpha_1 ~ \subt ~\alpha_2 }{?(\tilde{\tau}).\alpha_1 ~ \subt~ ?(\tilde{\sigma}).\alpha_2} 
\qquad
\inferrule[\rulename{s:InC}]{\beta_1 ~ \subt ~\beta_2  \qquad \alpha_1 ~ \subt ~\alpha_2 }{?(\beta_1).\alpha_1 ~ \subt ~?(\beta_2).\alpha_2} 
\quad  
&
 \\  
&
\inferrule[\rulename{s:OutE}]{\forall i.(\tau_i ~ \subt ~\sigma_i)  \qquad \alpha_1 ~ \subt ~\alpha_2 }{!(\tilde{\sigma}).\alpha_1 ~ \subt ~ !(\tilde{\tau}).\alpha_2} 
\qquad
\inferrule[\rulename{s:OutC} ]{\beta_1 ~ \subt ~\beta_2  \qquad \alpha_1 ~ \subt ~\alpha_2 }{!(\beta_2).\alpha_1 ~ \subt ~!(\beta_1).\alpha_2} 
&
\\
&
\inferrule[\rulename{s:Branch}]{\forall i \in \{1, \ldots, m\}. \alpha_i \subt \beta_i}{\&\{n_1:\alpha_1,\ldots, n_m:\alpha_m \} ~ \subt ~ \&\{n_1:\beta_1,\ldots, n_{m+j}:\beta_{m+j} \} } 
\quad  
&
 \\
 &
\inferrule[\rulename{s:Choice}]{\forall i \in \{1, \ldots, m\}. \alpha_i \subt \beta_i}{\oplus\{n_1:\alpha_1,\ldots, n_{m+j}:\alpha_{m+j} \} ~ \subt ~ \oplus\{n_1:\beta_1,\ldots, n_m:\beta_{m} \} } 
& 
\end{eqnarray*}
\caption{Subtyping rules. 
Intuitively, $\alpha \subt \beta$ is read as:
any process of type $\alpha$ can safely be used in a context where a process of type $\beta$ is expected.
} \label{tab:subt}
\end{table}

In the context of more stringent typing rules such as \rulename{t:MonAdapt}, it is convenient to find ways for relaxing the 
interface preorder \intpr in Def.~\ref{d:intpre}. 
As this preorder is central to our approach for disciplined runtime adaptation, 
a relaxed definition for it
may  lead to more flexible typing disciplines.
One alternative is to rely on
\emph{subtyping} for session types for such a relaxed definition.
We briefly recall the essential features of subtyping in session types; see~\cite{DBLP:journals/acta/GayH05,DBLP:journals/fuin/VallecilloVR06} for details. 
Given types $\alpha, \beta$, we say that 
$\alpha$ is a \emph{subtype} of $\beta$ (noted $\alpha \subt \beta$) 
if, 
intuitively, 
any process of type $\alpha$ can safely be used in a context where a process of type $\beta$ is expected. 
On basic types, subtyping arises from subset relations (as in, e.g., $\mathsf{int} \subt \mathsf{real}$).
For session types, $\subt$ is defined by the rules in Table~\ref{tab:subt}.
Observe how  $\subt$ is co-variant for input prefixes and contra-variant for outputs, 
whereas it is co-variant for branching and contra-variant for choices.

By relying on $\subt$, it is possible to define a more flexible preorder over interfaces:
\begin{definition}[Refined Interface Preorder] \label{d:rintpre}Given interfaces $\INT$ and $\INT'$, we write 
$\INT  \intpr_\text{sub} \INT'$ iff 
\begin{enumerate}[1.]
\item $\INT_\quau \subseteq \INT'_\quau$ and $\forall \inter{a}{\alpha}{h} \in \INT_\quau. \exists \inter{a}{\beta}{h} \in \INT'_\quau$ such that $\alpha \subt \beta$.
\item $\forall \inter{a}{\alpha}{h} \in \INT_\qual $  then 
$ \inter{a}{\beta}{h'} \in \INT'_\qual $, such that  $\alpha \subt \beta$ and \\ $h \leq h'$, for some $h'$.
\end{enumerate}
\end{definition}

It is immediate to see how $\intpr_\text{sub}$ improves over $\intpr$ by 
offering a more flexible and fine-grained relation over interfaces, in which subtyping replaces strict type equality.
We conjecture our main results (Theorems~\ref{t:safety} and \ref{t:consist}) 
would also hold, with little modifications, for the modified typing system 
that results by replacing 
\rulename{t:Adapt} with rule \rulename{t:MonAdapt} above, and by replacing \intpr  with $\intpr_\text{sub}$
in the appropriate places in Table~\ref{tab:ts}, 
Lemma~\ref{lem:substitution}(3), and Theorem~\ref{th:subred}.

 \section{Related Work}\label{sec:rw}




To our knowledge, ours is the first attempt to incorporate adaptation (or evolvability) constructs  into 
a session process language. 
Related to our work are efforts 
on formal models for service-oriented systems
with constructs such as exceptions and compensations (e.g.,~\cite{DBLP:conf/concur/CarboneHY08,DBLP:books/sp/sensoria2011/FerreiraLRVZ11}). 
In particular,~\cite{DBLP:conf/concur/CarboneHY08} develops a typeful approach for \emph{interactional exceptions}
in asynchronous session types. There, services define a default process and an exception handler, and may be influenced by 
a $\mathtt{throw}$ construct used to throw exceptions;
the goal of the typing system is to ensure consistent dynamic escaping from possibly nested exception scopes in a concerted way.

Notions 
such as exceptions and compensations are conceptually different from our intended notion of runtime adaptation.
In fact, in our view, such notions 
represent only a particular instance of adaptation/evolvabilty scenarios. 
This way, forms of exceptions (e.g., the one in~\cite{DBLP:conf/concur/CarboneHY08}) should typically handle \emph{internal events}
which  arise during the program's execution and may affect its flow of control. 
Similar in several respects to exceptions, mechanisms for compensations are usually conceived for 
handling events which are often exceptional \emph{and} catastrophic, such as runtime errors.
In contrast, runtime adaptation in modern distributed systems 
relies on \emph{external} mechanisms tailored to 
handle more general events, not necessarily catastrophic.
A familiar example of such events are program upgrades, whose execution can be anticipated and incorporated into the program's code for eventual execution. 
As another  example, consider elasticity in cloud-based applications, 
i.e., the ability such applications have to acquire/release computing resources based on user demand.
%depending on user activity, they determine how/when to .
%that in peaks of high activity additional computing resources must be acquired.
Although elasticity triggers 
%Such peaks, while triggering 
system adaptation, % of the system architecture, 
it does not represent a catastrophic event; rather, 
it represents an acceptable (yet hard to predict) state of the system.
Because of this conceptual difference, 
we do not have a clear perspective as to how 
known models of exceptions/compensations can be used to 
express the adaptation capabilities that 
are expressible in
our %session-typed 
framework. % is able to represent.

%\todo{
In contrast, more related to our approach is the recent work~\cite{DBLP:conf/aplas/AndersonR12}, 
where dynamic runtime update for message passing programs with queues is studied, 
and 
a form of consistency for updates over threads is ensured using 
multiparty session types.
As in our setting,
the notion of update in~\cite{DBLP:conf/aplas/AndersonR12} does not require
  a complete system shutdown, while ensuring that the state of the program remains consistent. There are significant 
  conceptual and technical differences between our work and~\cite{DBLP:conf/aplas/AndersonR12}. 
First, unlike our approach, in~\cite{DBLP:conf/aplas/AndersonR12} update actions (or adaptation routines)
are defined independently and externally from the program's syntax. 
Second,  here we have considered synchronous communication, 
whereas in~\cite{DBLP:conf/aplas/AndersonR12} an asynchronous thread model with queues is used.
Third, while we have analyzed updates for a language endowed with  binary session types, 
in~\cite{DBLP:conf/aplas/AndersonR12} the need for reaching agreements on multiple threads leads to the use of multiparty session 
types to ensure consistent updates.
It is instructive to note that approaches similar to ours can also be found in the sequential formalisms for reasoning at lower levels of abstraction. For instance, in \cite{DBLP:journals/toplas/StoyleHBSN07} the authors introduce dynamic updates to C-like languages, with a focus on runtime update of functions and type declarations. 
They show that dynamic updates are type-safe (consistent) as it cannot happen that different parts of the program expect
different representations of a type. Although the aim is similar, 
it is difficult to establish more precise comparisons, for our interest is in high-level reasoning for communicating programs with precise protocol descriptions.
%clearly, the setting is completely different as moving from a sequential to a concurrent scenario changes considerably the techniques and the problems to be solved.
%}
 In~\cite{DBLP:conf/amast/BrogiCP04} the authors also investigate behavioral types for adaptation, but 
 in the different setting of component-based systems.
Their notion of runtime adaptation %  \todo{different how?} 
relies on a notion of interface which describes the 
behavior of each component. These interfaces are to be used to implement inter-component communication. 
As it could that composition might not work because of  interface mismatching, 
the authors introduce the notion of  \emph{adaptors}, i.e., a software piece that  acts as mediator between two communicating components. It is interesting to notice that a similar mediator behavior could be implemented in our setting, as described in Sect. \ref{ss:behdist}.
%}



As already discussed, % along the paper, 
our approach has been influenced by~\cite{DBLP:conf/ppdp/GarraldaCD06} and our previous work~\cite{BGPZFMOODS}. 
Nevertheless, 
there are several major differences between 
our framework and those works. %~\cite{DBLP:conf/ppdp/GarraldaCD06}.
(1)~Unlike the system in~\cite{DBLP:conf/ppdp/GarraldaCD06}, our framework supports channel passing (delegation).
As delegation is already useful to 
represent forms of dynamic reconfiguration, its interplay with update actions is very appealing (cf. the example in Sect.~\ref{ss:behdist}).
%\jp{this is no longer useful} 
(2)~We have extended typing
judgments in~\cite{DBLP:conf/ppdp/GarraldaCD06} with \emph{interfaces} $\INT$, which are % of processes.
central to characterize located processes which can be safely updated. 
%with its two zones, $\Delta_l$ and $\Delta_u$. % and by the necessity of distinguishing between linear and unrestricted actions.
%Another distinctive feature of our approach is the treatment in the typing of the restriction operator. 
%In our setting, communication can happen at any level in the hierarchy of adaptable processes; hence, 
%in order to correctly type the number of active sessions (which, as discussed, is central to enable evolvability steps), the information on used session (e.g. $c:\bot$) cannot be hidden.
%Differences with respect to our previous work~\cite{BGPZFMOODS} are also important.
(3)~While in~\cite{BGPZFMOODS} adaptable processes are defined for a %(restriction-free) 
fragment of CCS, 
here we consider them within a typed $\pi$-calculus.
(4)~Adaptation steps in~\cite{BGPZFMOODS} are completely unrestricted. 
%i.e., an update will occur as soon as a located process and an update prefix are able to interact. 
Here we have considered annotated versions of the constructs in~\cite{BGPZFMOODS}:
% Here we have added two elements 
%which serve as a guard for enabling evolvability steps: the number of open sessions in the located processes
%and the interface $\Delta$, present both in the located process and in interacting update processes.
%we think that %our framework enhances the main insights of~\cite{BGPZFMOODS} by 
%they allow to represent evolvable, concurrent systems in a more realistic way, as
%taking the idea of adaptable process to a much more realistic setting, in which 
they offer a more realistic account of update actions, as they are supported 
by runtime conditions based on session types. %d, structured behavior. %determined by the runtime behavior of the system.





%\jp{Other related stuff: \cite{DBLP:conf/aplas/AndersonR12}, possibly also related: \cite{DBLP:conf/isola/LaneseM10,Ivan-Adaptive_C:2013}}
\section{Concluding Remarks}\label{sec:conc}
In this paper we have proposed a  framework for
%alternative \todo{approach?} for 
%specifying and 
reasoning about \emph{runtime ad\-ap\-ta\-tion} in the context of structured communications
described by session types.
Amalgamating a static analysis technique for correct communications (session types) 
with a novel, inherently dynamic form of interaction (as defined by update actions on located processes) is challenging, for 
it requires balancing two different (but equally important) concerns in modern interacting systems. 
In our approach, we investigated a session types discipline for an
extended $\pi$-calculus, in which channel mobility (delegation) is enhanced 
with the possibility of performing sophisticated update actions on located processes.
We purposefully aimed at integrating existing, well-studied lines of work: we expect this to be beneficial  for the 
enhancement of other known session types disciplines with adaptation concerns. 
In particular, we built upon our previous work on  
abstractions for evolvability in process calculi~\cite{BGPZFMOODS} and
on session types for mobile calculi~\cite{DBLP:conf/ppdp/GarraldaCD06}, relying also on 
a modern account of binary session types~\cite{DBLP:journals/entcs/YoshidaV07}.
In addition to runtime correctness (safety), our typing discipline
ensures consistency: this guarantees that communication behavior (as declared by types) is not disrupted by potential update actions.

%It is aimed at supporting the analysis of service-oriented applications/systems.





A main motivation for our work is the observation that while 
paradigms such as service-oriented computing are increasingly popular among practitioners, % software architects and programmers,
formal  models  based on them---such
%core programming calculi based on them---such
as reasoning techniques based on session types---fail to capture  
distinctive aspects of such par\-a\-digms.
Here we have aimed at addressing, for the first time, one of such aspects, namely runtime adaptation. 
In our view, it
%Here we have addressed one such aspects, runtime adaptation, 
represents an increasingly important concern when analyzing the behavior of communicating systems in 
%, which is intimately related to the fact that service oriented systemsare increasingly being deployed in very highly 
open, context-aware computing infrastructures.
%Our proposal, we believe, combines the most interesting aspects of these previous works in the context of the unexplored setting of evolvable session-typed processes. 
%\newpage
%
%As future work, we plan to investigate stronger notions of correctness for our adaptable, session-typed processes, in particular deadlock-freedom.
%Also, following~\cite{DBLP:journals/acta/GayH05} and the discussion in Sect.\ref{sec:int}, 
%we would like to integrate subtyping into our type system,
%and to obtain algorithmic characterizations
%of notions such as type duality and interface compatibility. 
%This work is an initial 
%step towards a theory of interaction
%in which processes---endowed with behavioral disciplines expressed as types---may dynamically evolve at runtime. 
In future work, we plan to investigate 
the interplay of adaptation with
issues such as subtyping, deadlock-freedom, resource usage, and trustworthiness, %, and reliability 
which are also important and challenging. %---we plan to look into these in the future. 
Nevertheless, we believe 
our work already contributes to the understanding of 
%that a major contribution of our paper %is novel, as it  is to address 
issues which, to our knowledge, have not yet  been explored in the realm of 
session-typed %interacting 
processes. 

% . \\%ways of enabling evolvability steps. \\
%-As future work, we plan to investigate stronger notions of correctness for adaptable, session-typed processes, and 
%to develop a formal treatment of subtyping and interface compatibility, along the discussion in Sect.\ref{sec:int}. \\%ways of enabling evolvability steps. \\



\paragraph{Acknowledgments}
%We thank 
%Ant\'{o}nio Ravara,
%Fabrizio Montesi, 
% and
%the SAC'13 and PLACES'13 
%anonymous reviewers for their useful and detailed remarks. 
This work was 
partially 
supported by the French projects 
ANR-11-INSE-0007- REVER and
ANR BLAN 0307 01 - SYNBIOTIC, as well as 
by the 
%Funda\c{c}\~{a}o para a Ci\^{e}ncia e a Tecnologia (
Portuguese Foundation for Science and Technology (FCT) %) 
through the Carnegie Mellon Portugal Program (grant
INTERFACES NGN-44 / 2009)
and grants  CITI and
SFRH\;/\;BPD\;/\;84067\;/\;2012.
 
%We thank the anonymous reviewers for their useful comments.



% 

{\small
\bibliographystyle{abbrv}
\bibliography{referen}
}

\end{document}